![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opelxp | Structured version Visualization version Unicode version |
Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opelxp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxp2 4870 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | vex 3059 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
3 | vex 3059 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
4 | 2, 3 | opth2 4693 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2527 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eleq1 2527 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | bi2anan9 889 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | sylbi 200 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | biimprcd 233 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | rexlimivv 2895 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | eqid 2461 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | opeq1 4179 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 12 | eqeq2d 2471 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | opeq2 4180 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 14 | eqeq2d 2471 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 13, 15 | rspc2ev 3172 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 11, 16 | mp3an3 1362 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 10, 17 | impbii 192 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 1, 18 | bitri 257 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-opab 4475 df-xp 4858 |
This theorem is referenced by: brxp 4883 opelxpi 4884 opelxp1 4885 opelxp2 4886 otel3xp 4888 opthprc 4900 elxp3 4903 opeliunxp 4904 bropaex12 4926 optocl 4929 xpsspw 4966 xpiindi 4988 opelres 5128 restidsing 5179 codir 5238 qfto 5239 xpnz 5274 difxp 5279 xpdifid 5283 ssrnres 5293 dfco2 5352 relssdmrn 5374 ressn 5390 elsnxp 5396 opelf 5767 oprab4 6388 resoprab 6418 oprssdm 6476 nssdmovg 6477 ndmovg 6478 elmpt2cl 6537 resiexg 6755 fo1stres 6843 fo2ndres 6844 el2xptp0 6863 dfoprab4 6876 opiota 6878 bropopvvv 6900 bropfvvvvlem 6901 curry1 6914 curry2 6917 xporderlem 6933 fnwelem 6937 mpt2xopxprcov0 6989 mpt2curryd 7041 brecop 7481 brecop2 7482 eceqoveq 7493 xpdom2 7692 mapunen 7766 dfac5lem2 8580 iunfo 8989 ordpipq 9392 prsrlem1 9521 opelcn 9578 opelreal 9579 elreal2 9581 swrd00 12810 swrdcl 12811 swrd0 12826 fsumcom2 13883 fprodcom2 14086 phimullem 14775 imasvscafn 15491 brcic 15751 homarcl2 15978 evlfcl 16155 clatl 16410 matplusgcell 19506 mdetrlin 19675 iscnp2 20303 txuni2 20628 txcls 20667 txcnpi 20671 txcnp 20683 txcnmpt 20687 txdis1cn 20698 txtube 20703 hausdiag 20708 txlm 20711 tx1stc 20713 txkgen 20715 txflf 21069 tmdcn2 21152 tgphaus 21179 qustgplem 21183 fmucndlem 21354 xmeterval 21495 metustexhalf 21619 blval2 21625 metuel2 21628 bcthlem1 22340 ovolfcl 22467 ovoliunlem1 22503 ovolshftlem1 22510 mbfimaopnlem 22659 limccnp2 22895 cxpcn3 23736 fsumvma 24189 lgsquadlem1 24330 lgsquadlem2 24331 2wlkonot3v 25651 2spthonot3v 25652 2wlkonotv 25653 numclwlk1lem2f 25868 ofresid 28291 xppreima2 28297 aciunf1lem 28312 f1od2 28357 smatrcl 28670 smatlem 28671 qtophaus 28711 esum2dlem 28961 eulerpartlemgvv 29257 erdszelem10 29971 cvmlift2lem10 30083 cvmlift2lem12 30085 msubff 30216 elmpst 30222 mpstrcl 30227 elmpps 30259 dfso2 30442 fv1stcnv 30470 fv2ndcnv 30471 txpss3v 30693 pprodss4v 30699 dfrdg4 30766 bj-elid3 31686 bj-eldiag2 31691 heiborlem3 32189 dibopelvalN 34755 dibopelval2 34757 dib1dim 34777 dihopcl 34865 dih1 34898 dih1dimatlem 34941 hdmap1val 35411 pellex 35723 elnonrel 36235 fourierdlem42 38049 fourierdlem42OLD 38050 etransclem44 38180 ovn0lem 38424 ndmaovg 38723 aoprssdm 38741 ndmaovcl 38742 ndmaovrcl 38743 ndmaovcom 38744 ndmaovass 38745 ndmaovdistr 38746 pfx00 38964 pfx0 38965 opeliun2xp 40386 |
Copyright terms: Public domain | W3C validator |