![]() |
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 5166 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) | |
2 | vex 3234 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
3 | vex 3234 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opth2 4978 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦)) |
5 | eleq1 2718 | . . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶)) | |
6 | eleq1 2718 | . . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) | |
7 | 5, 6 | bi2anan9 935 | . . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
8 | 4, 7 | sylbi 207 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
9 | 8 | biimprcd 240 | . . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))) |
10 | 9 | rexlimivv 3065 | . . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
11 | eqid 2651 | . . . 4 ⊢ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 | |
12 | opeq1 4433 | . . . . . 6 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
13 | 12 | eqeq2d 2661 | . . . . 5 ⊢ (𝑥 = 𝐴 → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉)) |
14 | opeq2 4434 | . . . . . 6 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
15 | 14 | eqeq2d 2661 | . . . . 5 ⊢ (𝑦 = 𝐵 → (〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉)) |
16 | 13, 15 | rspc2ev 3355 | . . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
17 | 11, 16 | mp3an3 1453 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
18 | 10, 17 | impbii 199 | . 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
19 | 1, 18 | bitri 264 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∃wrex 2942 〈cop 4216 × cxp 5141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-opab 4746 df-xp 5149 |
This theorem is referenced by: brxp 5181 opelxpi 5182 opelxp1 5184 opelxp2 5185 otel3xp 5187 opthprc 5201 elxp3 5203 opeliunxp 5204 bropaex12 5226 optocl 5229 xpsspw 5266 xpiindi 5290 opelresg 5434 opelresOLD 5438 restidsing 5493 restidsingOLD 5494 codir 5551 qfto 5552 xpnz 5588 difxp 5593 xpdifid 5597 ssrnres 5607 dfco2 5672 relssdmrn 5694 ressn 5709 elsnxpOLD 5716 opelf 6103 oprab4 6768 resoprab 6798 oprssdm 6857 nssdmovg 6858 ndmovg 6859 elmpt2cl 6918 resiexg 7144 fo1stres 7236 fo2ndres 7237 el2xptp0 7256 dfoprab4 7269 opiota 7273 bropopvvv 7300 bropfvvvvlem 7301 curry1 7314 curry2 7317 xporderlem 7333 fnwelem 7337 mpt2xopxprcov0 7388 mpt2curryd 7440 brecop 7883 brecop2 7884 eceqoveq 7895 xpdom2 8096 mapunen 8170 dfac5lem2 8985 iunfo 9399 ordpipq 9802 prsrlem1 9931 opelcn 9988 opelreal 9989 elreal2 9991 swrd00 13463 swrdcl 13464 swrd0 13480 fsumcom2 14549 fsumcom2OLD 14550 fprodcom2 14758 fprodcom2OLD 14759 phimullem 15531 imasvscafn 16244 brcic 16505 homarcl2 16732 evlfcl 16909 clatl 17163 matplusgcell 20287 mdetrlin 20456 iscnp2 21091 txuni2 21416 txcls 21455 txcnpi 21459 txcnp 21471 txcnmpt 21475 txdis1cn 21486 txtube 21491 hausdiag 21496 txlm 21499 tx1stc 21501 txkgen 21503 txflf 21857 tmdcn2 21940 tgphaus 21967 qustgplem 21971 fmucndlem 22142 xmeterval 22284 metustexhalf 22408 blval2 22414 metuel2 22417 bcthlem1 23167 ovolfcl 23281 ovoliunlem1 23316 ovolshftlem1 23323 mbfimaopnlem 23467 limccnp2 23701 cxpcn3 24534 fsumvma 24983 lgsquadlem1 25150 lgsquadlem2 25151 ofresid 29572 xppreima2 29578 aciunf1lem 29590 f1od2 29627 smatrcl 29990 smatlem 29991 qtophaus 30031 eulerpartlemgvv 30566 erdszelem10 31308 cvmlift2lem10 31420 cvmlift2lem12 31422 msubff 31553 elmpst 31559 mpstrcl 31564 elmpps 31596 dfso2 31770 fv1stcnv 31804 fv2ndcnv 31805 txpss3v 32110 pprodss4v 32116 dfrdg4 32183 bj-elid3 33217 bj-eldiag2 33222 curf 33517 curunc 33521 heiborlem3 33742 opelresALTV 34172 xrnss3v 34274 inxpxrn 34293 dibopelvalN 36749 dibopelval2 36751 dib1dim 36771 dihopcl 36859 dih1 36892 dih1dimatlem 36935 hdmap1val 37405 pellex 37716 elnonrel 38208 fourierdlem42 40684 etransclem44 40813 ovn0lem 41100 ndmaovg 41585 aoprssdm 41603 ndmaovcl 41604 ndmaovrcl 41605 ndmaovcom 41606 ndmaovass 41607 ndmaovdistr 41608 pfx00 41709 pfx0 41710 sprsymrelfvlem 42065 sprsymrelfolem2 42068 opeliun2xp 42436 |
Copyright terms: Public domain | W3C validator |