Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opelxp | Structured version Visualization version GIF 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 5056 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) | |
2 | vex 3176 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
3 | vex 3176 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opth2 4875 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦)) |
5 | eleq1 2676 | . . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶)) | |
6 | eleq1 2676 | . . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) | |
7 | 5, 6 | bi2anan9 913 | . . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
8 | 4, 7 | sylbi 206 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
9 | 8 | biimprcd 239 | . . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))) |
10 | 9 | rexlimivv 3018 | . . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
11 | eqid 2610 | . . . 4 ⊢ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 | |
12 | opeq1 4340 | . . . . . 6 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
13 | 12 | eqeq2d 2620 | . . . . 5 ⊢ (𝑥 = 𝐴 → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉)) |
14 | opeq2 4341 | . . . . . 6 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
15 | 14 | eqeq2d 2620 | . . . . 5 ⊢ (𝑦 = 𝐵 → (〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉)) |
16 | 13, 15 | rspc2ev 3295 | . . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
17 | 11, 16 | mp3an3 1405 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
18 | 10, 17 | impbii 198 | . 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
19 | 1, 18 | bitri 263 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∃wrex 2897 〈cop 4131 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-opab 4644 df-xp 5044 |
This theorem is referenced by: brxp 5071 opelxpi 5072 opelxp1 5074 opelxp2 5075 otel3xp 5077 opthprc 5089 elxp3 5092 opeliunxp 5093 bropaex12 5115 optocl 5118 xpsspw 5156 xpiindi 5179 opelres 5322 restidsing 5377 restidsingOLD 5378 codir 5435 qfto 5436 xpnz 5472 difxp 5477 xpdifid 5481 ssrnres 5491 dfco2 5551 relssdmrn 5573 ressn 5588 elsnxpOLD 5595 opelf 5978 oprab4 6624 resoprab 6654 oprssdm 6713 nssdmovg 6714 ndmovg 6715 elmpt2cl 6774 resiexg 6994 fo1stres 7083 fo2ndres 7084 el2xptp0 7103 dfoprab4 7116 opiota 7118 bropopvvv 7142 bropfvvvvlem 7143 curry1 7156 curry2 7159 xporderlem 7175 fnwelem 7179 mpt2xopxprcov0 7230 mpt2curryd 7282 brecop 7727 brecop2 7728 eceqoveq 7740 xpdom2 7940 mapunen 8014 dfac5lem2 8830 iunfo 9240 ordpipq 9643 prsrlem1 9772 opelcn 9829 opelreal 9830 elreal2 9832 swrd00 13270 swrdcl 13271 swrd0 13286 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 phimullem 15322 imasvscafn 16020 brcic 16281 homarcl2 16508 evlfcl 16685 clatl 16939 matplusgcell 20058 mdetrlin 20227 iscnp2 20853 txuni2 21178 txcls 21217 txcnpi 21221 txcnp 21233 txcnmpt 21237 txdis1cn 21248 txtube 21253 hausdiag 21258 txlm 21261 tx1stc 21263 txkgen 21265 txflf 21620 tmdcn2 21703 tgphaus 21730 qustgplem 21734 fmucndlem 21905 xmeterval 22047 metustexhalf 22171 blval2 22177 metuel2 22180 bcthlem1 22929 ovolfcl 23042 ovoliunlem1 23077 ovolshftlem1 23084 mbfimaopnlem 23228 limccnp2 23462 cxpcn3 24289 fsumvma 24738 lgsquadlem1 24905 lgsquadlem2 24906 2wlkonot3v 26402 2spthonot3v 26403 2wlkonotv 26404 numclwlk1lem2f 26619 ofresid 28824 xppreima2 28830 aciunf1lem 28844 f1od2 28887 smatrcl 29190 smatlem 29191 qtophaus 29231 eulerpartlemgvv 29765 erdszelem10 30436 cvmlift2lem10 30548 cvmlift2lem12 30550 msubff 30681 elmpst 30687 mpstrcl 30692 elmpps 30724 dfso2 30897 fv1stcnv 30925 fv2ndcnv 30926 txpss3v 31155 pprodss4v 31161 dfrdg4 31228 bj-elid3 32264 bj-eldiag2 32269 curf 32557 curunc 32561 heiborlem3 32782 dibopelvalN 35450 dibopelval2 35452 dib1dim 35472 dihopcl 35560 dih1 35593 dih1dimatlem 35636 hdmap1val 36106 pellex 36417 elnonrel 36910 fourierdlem42 39042 etransclem44 39171 ovn0lem 39455 ndmaovg 39913 aoprssdm 39931 ndmaovcl 39932 ndmaovrcl 39933 ndmaovcom 39934 ndmaovass 39935 ndmaovdistr 39936 pfx00 40247 pfx0 40248 opeliun2xp 41904 |
Copyright terms: Public domain | W3C validator |