Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > opeq2 | Unicode version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opeq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2202 | . . . . . 6 | |
2 | 1 | anbi2d 459 | . . . . 5 |
3 | eqidd 2140 | . . . . . . 7 | |
4 | preq2 3601 | . . . . . . 7 | |
5 | 3, 4 | preq12d 3608 | . . . . . 6 |
6 | 5 | eleq2d 2209 | . . . . 5 |
7 | 2, 6 | anbi12d 464 | . . . 4 |
8 | df-3an 964 | . . . 4 | |
9 | df-3an 964 | . . . 4 | |
10 | 7, 8, 9 | 3bitr4g 222 | . . 3 |
11 | 10 | abbidv 2257 | . 2 |
12 | df-op 3536 | . 2 | |
13 | df-op 3536 | . 2 | |
14 | 11, 12, 13 | 3eqtr4g 2197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 wceq 1331 wcel 1480 cab 2125 cvv 2686 csn 3527 cpr 3528 cop 3530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 |
This theorem is referenced by: opeq12 3707 opeq2i 3709 opeq2d 3712 oteq2 3715 oteq3 3716 breq2 3933 cbvopab2 4002 cbvopab2v 4005 opthg 4160 eqvinop 4165 opelopabsb 4182 opelxp 4569 opabid2 4670 elrn2g 4729 opeldm 4742 opeldmg 4744 elrn2 4781 opelresg 4826 iss 4865 elimasng 4907 issref 4921 dmsnopg 5010 cnvsng 5024 elxp4 5026 elxp5 5027 dffun5r 5135 funopg 5157 f1osng 5408 tz6.12f 5450 fsn 5592 fsng 5593 fvsng 5616 oveq2 5782 cbvoprab2 5844 ovg 5909 opabex3d 6019 opabex3 6020 op1stg 6048 op2ndg 6049 oprssdmm 6069 op1steq 6077 dfoprab4f 6091 tfrlemibxssdm 6224 tfr1onlembxssdm 6240 tfrcllembxssdm 6253 elixpsn 6629 ixpsnf1o 6630 mapsnen 6705 xpsnen 6715 xpassen 6724 xpf1o 6738 djulclr 6934 djurclr 6935 djulcl 6936 djurcl 6937 djulclb 6940 inl11 6950 djuss 6955 1stinl 6959 2ndinl 6960 1stinr 6961 2ndinr 6962 elreal 7636 ax1rid 7685 fseq1p1m1 9874 cnmpt21 12460 djucllem 13007 |
Copyright terms: Public domain | W3C validator |