![]() |
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 2518 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1d 716 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sneq 3946 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | preq1 4020 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | preq12d 4028 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | ifbieq1d 3872 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | dfopif 4133 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | dfopif 4133 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 6, 7, 8 | 3eqtr4g 2511 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-rab 2746 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 |
This theorem is referenced by: opeq12 4138 opeq1i 4139 opeq1d 4142 oteq1 4145 breq1 4377 cbvopab1 4445 cbvopab1s 4447 opthg 4650 eqvinop 4659 opelopabsb 4684 opelxp 4842 elvvv 4872 opabid2 4942 opeliunxp2 4951 elsnres 5119 elimasng 5172 dmsnopg 5286 cnvsng 5301 elsnxp 5357 funopg 5593 f1osng 5836 f1oprswap 5837 dmfco 5923 fvelrn 5999 fsng 6048 fprg 6058 fvrnressn 6064 fvsng 6083 funfvima3 6128 oveq1 6283 oprabid 6303 dfoprab2 6325 cbvoprab1 6351 elxp4 6725 elxp5 6726 opabex3d 6759 opabex3 6760 op1stg 6793 op2ndg 6794 el2xptp 6824 dfoprab4f 6839 frxp 6894 opeliunxp2f 6944 tfrlem11 7093 omeu 7273 oeeui 7290 elixpsn 7548 fundmen 7630 xpsnen 7643 xpassen 7653 xpf1o 7721 unxpdomlem1 7763 dfac5lem1 8541 dfac5lem4 8544 axdc4lem 8872 nqereu 9341 mulcanenq 9372 archnq 9392 prlem934 9445 supsrlem 9522 supsr 9523 swrdccatin1 12838 swrdccat3blem 12850 fsum2dlem 13842 fprod2dlem 14045 vdwlem10 14951 imasaddfnlem 15445 catideu 15592 iscatd2 15598 catlid 15600 catpropd 15625 symg2bas 17050 efgmval 17373 efgi 17380 vrgpval 17428 gsumcom2 17618 txkgen 20678 cnmpt21 20697 xkoinjcn 20713 txcon 20715 pt1hmeo 20832 cnextfvval 21091 qustgplem 21146 dvbsss 22869 axlowdim2 25002 axlowdim 25003 axcontlem10 25015 axcontlem12 25017 0eusgraiff0rgra 25679 drngoi 26147 isdivrngo 26171 isnvlem 26241 br8d 28227 cnvoprab 28316 prsrn 28728 esum2dlem 28920 eulerpartlemgvv 29215 br8 30402 br6 30403 br4 30404 eldm3 30408 br1steqg 30422 br2ndeqg 30423 dfdm5 30424 elfuns 30688 brimg 30710 brapply 30711 brsuccf 30714 brrestrict 30722 dfrdg4 30724 cgrdegen 30777 brofs 30778 cgrextend 30781 brifs 30816 ifscgr 30817 brcgr3 30819 brcolinear2 30831 colineardim1 30834 brfs 30852 idinside 30857 btwnconn1lem7 30866 btwnconn1lem11 30870 btwnconn1lem12 30871 brsegle 30881 outsideofeu 30904 fvray 30914 linedegen 30916 fvline 30917 bj-inftyexpiinv 31652 bj-inftyexpidisj 31654 finxpeq2 31781 finxpreclem6 31790 finxpsuclem 31791 dicelval3 34750 dihjatcclem4 34991 dropab1 36801 relopabVD 37295 |
Copyright terms: Public domain | W3C validator |