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 2100 | . . . . . 6 | |
2 | 1 | anbi2d 437 | . . . . 5 |
3 | eqidd 2041 | . . . . . . 7 | |
4 | preq2 3448 | . . . . . . 7 | |
5 | 3, 4 | preq12d 3455 | . . . . . 6 |
6 | 5 | eleq2d 2107 | . . . . 5 |
7 | 2, 6 | anbi12d 442 | . . . 4 |
8 | df-3an 887 | . . . 4 | |
9 | df-3an 887 | . . . 4 | |
10 | 7, 8, 9 | 3bitr4g 212 | . . 3 |
11 | 10 | abbidv 2155 | . 2 |
12 | df-op 3384 | . 2 | |
13 | df-op 3384 | . 2 | |
14 | 11, 12, 13 | 3eqtr4g 2097 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 wceq 1243 wcel 1393 cab 2026 cvv 2557 csn 3375 cpr 3376 cop 3378 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-un 2922 df-sn 3381 df-pr 3382 df-op 3384 |
This theorem is referenced by: opeq12 3551 opeq2i 3553 opeq2d 3556 oteq2 3559 oteq3 3560 breq2 3768 cbvopab2 3831 cbvopab2v 3834 opthg 3975 eqvinop 3980 opelopabsb 3997 opelxp 4374 opabid2 4467 elrn2g 4525 opeldm 4538 opeldmg 4540 elrn2 4576 opelresg 4619 iss 4654 elimasng 4693 issref 4707 dmsnopg 4792 cnvsng 4806 elxp4 4808 elxp5 4809 dffun5r 4914 funopg 4934 f1osng 5167 tz6.12f 5202 fsn 5335 fsng 5336 fvsng 5359 oveq2 5520 cbvoprab2 5577 ovg 5639 opabex3d 5748 opabex3 5749 op1stg 5777 op2ndg 5778 op1steq 5805 dfoprab4f 5819 tfrlemibxssdm 5941 xpsnen 6295 xpassen 6304 elreal 6905 ax1rid 6951 fseq1p1m1 8956 |
Copyright terms: Public domain | W3C validator |