Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opeq1d | Structured version Visualization version Unicode version |
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1d.1 |
Ref | Expression |
---|---|
opeq1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1d.1 | . 2 | |
2 | opeq1 4402 | . 2 | |
3 | 1, 2 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 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: oteq1 4411 oteq2 4412 opth 4945 elsnxp 5677 cbvoprab2 6728 unxpdomlem1 8164 mulcanenq 9782 ax1rid 9982 axrnegex 9983 fseq1m1p1 12415 uzrdglem 12756 swrd0swrd 13461 swrdccat 13493 swrdccat3a 13494 swrdccat3blem 13495 cshw0 13540 cshwmodn 13541 s2prop 13652 s4prop 13655 fsum2dlem 14501 fprod2dlem 14710 ruclem1 14960 imasaddvallem 16189 iscatd2 16342 moni 16396 homadmcd 16692 curf1 16865 curf1cl 16868 curf2 16869 hofcl 16899 gsum2dlem2 18370 imasdsf1olem 22178 ovoliunlem1 23270 cxpcn3 24489 axlowdimlem15 25836 axlowdim 25841 nvi 27469 nvop 27531 phop 27673 br8d 29422 fgreu 29471 1stpreimas 29483 smatfval 29861 smatrcl 29862 smatlem 29863 fvproj 29899 mvhfval 31430 mpst123 31437 br8 31646 nosupbnd2 31862 fvtransport 32139 rfovcnvf1od 38298 |
Copyright terms: Public domain | W3C validator |