New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > opeq1 | Unicode version |
Description: Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.) |
Ref | Expression |
---|---|
opeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imakeq2 4225 | . . 3 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 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 | |
2 | 1 | uneq1d 3417 | . 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-1 5 ax-2 6 ax-3 7 ax-mp 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 opeq1i 4581 opeq1d 4584 eqvinop 4606 cbvopab1 4632 cbvopab1s 4634 breq1 4642 opelopabsb 4697 el1st 4729 br1stg 4730 elswap 4740 dfima2 4745 dfco1 4748 dfsi2 4751 opeliunxp2 4822 ssrel 4844 ssopr 4846 br1st 4858 brswap2 4860 opabid2 4861 elsnres 4996 elxp4 5108 dfxp2 5113 fnunsn 5190 f1osng 5323 fvelrn 5413 fsng 5433 fvsng 5446 oveq1 5530 oprabid 5550 dfoprab2 5558 cbvoprab1 5567 oprabid2 5646 trtxp 5781 brtxp 5783 otelins2 5791 otelins3 5792 oqelins4 5794 qrpprod 5836 xpassen 6057 addccan2nclem1 6262 |
Copyright terms: Public domain | W3C validator |