New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > opeq2 | Unicode version |
Description: Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.) |
Ref | Expression |
---|---|
opeq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imakeq2 4225 | . . 3 ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck | |
2 | 1 | uneq2d 3418 | . 2 ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck |
3 | dfop2 4575 | . 2 ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck | |
4 | dfop2 4575 | . 2 ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck | |
5 | 2, 3, 4 | 3eqtr4g 2410 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1642 cvv 2859 ∼ ccompl 3205 cdif 3206 cun 3207 cin 3208 csymdif 3209 csn 3737 1cc1c 4134 1 cpw1 4135 k cxpk 4174 kccnvk 4175 Ins2k cins2k 4176 Ins3k cins3k 4177 kcimak 4179 k ccomk 4180 SIk csik 4181 Imagekcimagek 4182 Sk cssetk 4183 k cidk 4184 Nn cnnc 4373 0cc0c 4374 cop 4561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-addc 4378 df-nnc 4379 df-phi 4565 df-op 4566 |
This theorem is referenced by: opeq12 4580 opeq2i 4582 opeq2d 4585 eqvinop 4606 cbvopab2 4633 cbvopab2v 4636 breq2 4643 opelopabsb 4697 br1stg 4730 elswap 4740 dfima2 4745 dfco1 4748 dfsi2 4751 dfid3 4768 ssrel 4844 br2nd 4859 brswap2 4860 opabid2 4861 opeldm 4910 iss 5000 dmsnopg 5066 elxp4 5108 dfxp2 5113 nfunv 5138 fnunsn 5190 iunfopab 5204 f1osng 5323 fsn 5432 fsng 5433 fvsng 5446 xpnedisj 5513 oveq2 5531 cbvoprab2 5568 oprabid2 5646 trtxp 5781 brtxp 5783 oqelins4 5794 txpcofun 5803 addcfnex 5824 qrpprod 5836 fundmen 6043 xpassen 6057 addccan2nclem1 6263 freceq12 6311 |
Copyright terms: Public domain | W3C validator |