![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > opelxp | Structured 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 4956 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | vex 3071 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
3 | vex 3071 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
4 | 2, 3 | opth2 4668 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2523 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eleq1 2523 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | bi2anan9 868 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | sylbi 195 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | biimprcd 225 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | rexlimivv 2942 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | eqid 2451 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | opeq1 4157 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 12 | eqeq2d 2465 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | opeq2 4158 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 14 | eqeq2d 2465 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 13, 15 | rspc2ev 3178 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 11, 16 | mp3an3 1304 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 10, 17 | impbii 188 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 1, 18 | bitri 249 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4511 ax-nul 4519 ax-pr 4629 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3070 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-nul 3736 df-if 3890 df-sn 3976 df-pr 3978 df-op 3982 df-opab 4449 df-xp 4944 |
This theorem is referenced by: brxp 4968 opelxpi 4969 opelxp1 4970 opelxp2 4971 opthprc 4984 elxp3 4987 opeliunxp 4988 optocl 5011 xpsspwOLD 5052 xpiindi 5073 opelres 5214 restidsing 5260 codir 5316 qfto 5317 xpnz 5355 difxp 5360 xpdifid 5364 ssrnres 5374 dfco2 5435 relssdmrn 5456 ressn 5471 opelf 5672 oprab4 6256 resoprab 6286 oprssdm 6344 nssdmovg 6345 ndmovg 6346 elmpt2cl 6404 resiexg 6614 fo1stres 6700 fo2ndres 6701 dfoprab4 6731 opiota 6733 bropopvvv 6753 curry1 6764 curry2 6767 xporderlem 6783 fnwelem 6787 mpt2xopxprcov0 6834 mpt2curryd 6888 brecop 7293 brecop2 7294 eceqoveq 7305 xpdom2 7506 mapunen 7580 dfac5lem2 8395 iunfo 8804 ordpipq 9212 opelcn 9397 opelreal 9398 elreal2 9400 swrd00 12416 swrdcl 12417 swrd0 12429 fsumcom2 13343 phimullem 13956 imasvscafn 14577 homarcl2 15005 evlfcl 15134 clatl 15388 mdetrlin 18524 iscnp2 18959 txuni2 19254 txcls 19293 txcnpi 19297 txcnp 19309 txcnmpt 19313 txdis1cn 19324 txtube 19329 hausdiag 19334 txlm 19337 tx1stc 19339 txkgen 19341 txflf 19695 tmdcn2 19776 tgphaus 19803 divstgplem 19807 fmucndlem 19982 xmeterval 20123 metustexhalfOLD 20254 metustexhalf 20255 blval2 20266 metuel2 20270 bcthlem1 20951 ovolfcl 21066 ovoliunlem1 21101 ovolshftlem1 21108 mbfimaopnlem 21249 limccnp2 21483 cxpcn3 22302 fsumvma 22668 lgsquadlem1 22809 lgsquadlem2 22810 ofresid 26094 xppreima2 26099 f1od2 26158 eulerpartlemgvv 26893 erdszelem10 27222 cvmlift2lem10 27335 cvmlift2lem12 27337 fprodcom2 27629 dfso2 27698 txpss3v 28043 pprodss4v 28049 dfrdg4 28115 heiborlem3 28850 pellex 29314 ndmaovg 30228 aoprssdm 30246 ndmaovcl 30247 ndmaovrcl 30248 ndmaovcom 30249 ndmaovass 30250 ndmaovdistr 30251 el2xptp0 30265 otel3xp 30266 2wlkonot3v 30532 2spthonot3v 30533 2wlkonotv 30534 numclwlk1lem2f 30823 opeliun2xp 30858 matplusgcell 31005 dibopelvalN 35094 dibopelval2 35096 dib1dim 35116 dihopcl 35204 dih1 35237 dih1dimatlem 35280 hdmap1val 35750 |
Copyright terms: Public domain | W3C validator |