Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opeq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2689 | . . . 4 | |
2 | 1 | anbi1d 741 | . . 3 |
3 | sneq 4187 | . . . 4 | |
4 | preq1 4268 | . . . 4 | |
5 | 3, 4 | preq12d 4276 | . . 3 |
6 | 2, 5 | ifbieq1d 4109 | . 2 |
7 | dfopif 4399 | . 2 | |
8 | dfopif 4399 | . 2 | |
9 | 6, 7, 8 | 3eqtr4g 2681 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wcel 1990 cvv 3200 c0 3915 cif 4086 csn 4177 cpr 4179 cop 4183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 |
This theorem is referenced by: opeq12 4404 opeq1i 4405 opeq1d 4408 oteq1 4411 breq1 4656 cbvopab1 4723 cbvopab1s 4725 opthg 4946 eqvinop 4955 opelopabsb 4985 opelxp 5146 elvvv 5178 opabid2 5251 opeliunxp2 5260 elsnres 5436 elimasng 5491 dmsnopg 5606 cnvsng 5621 elsnxpOLD 5678 funopg 5922 f1osng 6177 f1oprswap 6180 dmfco 6272 fvelrn 6352 fsng 6404 fprg 6422 fvrnressn 6428 fvsng 6447 funfvima3 6495 oveq1 6657 oprabid 6677 dfoprab2 6701 cbvoprab1 6727 elxp4 7110 elxp5 7111 opabex3d 7145 opabex3 7146 op1stg 7180 op2ndg 7181 el2xptp 7211 dfoprab4f 7226 frxp 7287 opeliunxp2f 7336 tfrlem11 7484 omeu 7665 oeeui 7682 elixpsn 7947 fundmen 8030 xpsnen 8044 xpassen 8054 xpf1o 8122 unxpdomlem1 8164 dfac5lem1 8946 dfac5lem4 8949 axdc4lem 9277 nqereu 9751 mulcanenq 9782 archnq 9802 prlem934 9855 supsrlem 9932 supsr 9933 swrdccatin1 13483 swrdccat3blem 13495 fsum2dlem 14501 fprod2dlem 14710 vdwlem10 15694 imasaddfnlem 16188 catideu 16336 iscatd2 16342 catlid 16344 catpropd 16369 symg2bas 17818 efgmval 18125 efgi 18132 vrgpval 18180 gsumcom2 18374 txkgen 21455 cnmpt21 21474 xkoinjcn 21490 txconn 21492 pt1hmeo 21609 cnextfvval 21869 qustgplem 21924 dvbsss 23666 axlowdim2 25840 axlowdim 25841 axcontlem10 25853 axcontlem12 25855 isnvlem 27465 br8d 29422 cnvoprab 29498 prsrn 29961 esum2dlem 30154 eulerpartlemgvv 30438 br8 31646 br6 31647 br4 31648 eldm3 31651 br1steqgOLD 31674 br2ndeqgOLD 31675 dfdm5 31676 elfuns 32022 brimg 32044 brapply 32045 brsuccf 32048 brrestrict 32056 dfrdg4 32058 cgrdegen 32111 brofs 32112 cgrextend 32115 brifs 32150 ifscgr 32151 brcgr3 32153 brcolinear2 32165 colineardim1 32168 brfs 32186 idinside 32191 btwnconn1lem7 32200 btwnconn1lem11 32204 btwnconn1lem12 32205 brsegle 32215 outsideofeu 32238 fvray 32248 linedegen 32250 fvline 32251 bj-inftyexpiinv 33095 bj-inftyexpidisj 33097 finxpeq2 33224 finxpreclem6 33233 finxpsuclem 33234 curfv 33389 isdivrngo 33749 drngoi 33750 dicelval3 36469 dihjatcclem4 36710 dropab1 38651 relopabVD 39137 |
Copyright terms: Public domain | W3C validator |