| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. |
| Ref | Expression |
|---|---|
| funfvop |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvex 4500 |
. . 3
| |
| 2 | 1 | isseti 2130 |
. 2
|
| 3 | visset 2128 |
. . . . . . 7
| |
| 4 | 3 | funopfvb 4526 |
. . . . . 6
|
| 5 | opeq2 2981 |
. . . . . . . 8
| |
| 6 | 5 | eleq1d 1800 |
. . . . . . 7
|
| 7 | 6 | biimprcd 172 |
. . . . . 6
|
| 8 | 4, 7 | syl6bi 230 |
. . . . 5
|
| 9 | 8 | pm2.43d 79 |
. . . 4
|
| 10 | eqcom 1723 |
. . . 4
| |
| 11 | 9, 10 | syl5ib 222 |
. . 3
|
| 12 | 11 | 19.23adv 1422 |
. 2
|
| 13 | 2, 12 | mpi 55 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: fvimacnv 4589 fnopfv 4595 fvelrn 4596 dff3 4601 funfvima3 4641 fundmen 5298 adj1 11286 bnj143 12267 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1142 ax-gen 1143 ax-8 1144 ax-9 1145 ax-10 1146 ax-11 1147 ax-12 1148 ax-13 1149 ax-14 1150 ax-17 1155 ax-4 1157 ax-5o 1159 ax-6o 1162 ax-9o 1319 ax-10o 1338 ax-16 1418 ax-11o 1426 ax-ext 1702 ax-sep 3253 ax-nul 3260 ax-pow 3296 ax-pr 3339 ax-un 3601 |
| This theorem depends on definitions: df-bi 163 df-or 240 df-an 241 df-ex 1165 df-sb 1374 df-eu 1613 df-mo 1614 df-clab 1709 df-cleq 1714 df-clel 1717 df-ne 1856 df-rex 1944 df-v 2127 df-dif 2430 df-un 2433 df-in 2436 df-ss 2438 df-nul 2702 df-pw 2859 df-sn 2873 df-pr 2874 df-op 2877 df-uni 3000 df-br 3159 df-opab 3214 df-id 3401 df-xp 3811 df-cnv 3813 df-co 3814 df-dm 3815 df-rn 3816 df-res 3817 df-ima 3818 df-fun 3819 df-fn 3820 df-fv 3825 |