![]() |
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 5432 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) | |
2 | vex 3418 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
3 | vex 3418 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | opth2 5230 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦)) |
5 | eleq1 2853 | . . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶)) | |
6 | eleq1 2853 | . . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷)) | |
7 | 5, 6 | bi2anan9 626 | . . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
8 | 4, 7 | sylbi 209 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
9 | 8 | biimprcd 242 | . . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))) |
10 | 9 | rexlimivv 3237 | . . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
11 | eqid 2778 | . . . 4 ⊢ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 | |
12 | opeq1 4678 | . . . . . 6 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
13 | 12 | eqeq2d 2788 | . . . . 5 ⊢ (𝑥 = 𝐴 → (〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉)) |
14 | opeq2 4679 | . . . . . 6 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
15 | 14 | eqeq2d 2788 | . . . . 5 ⊢ (𝑦 = 𝐵 → (〈𝐴, 𝐵〉 = 〈𝐴, 𝑦〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉)) |
16 | 13, 15 | rspc2ev 3550 | . . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
17 | 11, 16 | mp3an3 1429 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉) |
18 | 10, 17 | impbii 201 | . 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
19 | 1, 18 | bitri 267 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∃wrex 3089 〈cop 4448 × cxp 5406 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-opab 4993 df-xp 5414 |
This theorem is referenced by: opelxpi 5445 opelxp1 5449 opelxp2 5450 otel3xp 5452 brxp 5454 opthprc 5467 elxp3 5469 opeliunxp 5470 bropaex12 5493 optocl 5496 xpsspw 5533 xpiindi 5557 opelres 5702 opelresgOLD2 5706 restidsing 5766 codir 5822 qfto 5823 xpnz 5858 difxp 5863 xpdifid 5867 dfco2 5939 relssdmrn 5961 ressn 5976 opelf 6370 oprab4 7058 resoprab 7088 oprssdm 7147 nssdmovg 7148 ndmovg 7149 elmpocl 7208 fo1stres 7529 fo2ndres 7530 dfoprab4 7563 opiota 7567 bropopvvv 7595 bropfvvvvlem 7596 curry1 7609 xporderlem 7628 fnwelem 7632 mpoxopxprcov0 7688 mpocurryd 7740 brecop 8192 brecop2 8193 eceqoveq 8204 xpdom2 8410 mapunen 8484 djuss 9145 djuunxp 9146 dfac5lem2 9346 iunfo 9761 ordpipq 10164 prsrlem1 10294 opelcn 10351 opelreal 10352 elreal2 10354 swrdnznd 13808 swrd00 13810 swrdcl 13811 swrd0 13829 pfx00 13859 pfx0 13860 fsumcom2 14992 fprodcom2 15201 phimullem 15975 imasvscafn 16669 homarcl2 17156 evlfcl 17333 clatl 17587 matplusgcell 20749 iscnp2 21554 txuni2 21880 txcls 21919 txcnpi 21923 txcnp 21935 txcnmpt 21939 txdis1cn 21950 txtube 21955 hausdiag 21960 txlm 21963 tx1stc 21965 txkgen 21967 txflf 22321 tmdcn2 22404 tgphaus 22431 qustgplem 22435 fmucndlem 22606 xmeterval 22748 metustexhalf 22872 blval2 22878 bcthlem1 23633 ovolfcl 23773 ovoliunlem1 23809 mbfimaopnlem 23962 limccnp2 24196 fsumvma 25494 lgsquadlem1 25661 lgsquadlem2 25662 dmrab 30042 xppreima2 30160 aciunf1lem 30172 f1od2 30212 smatrcl 30703 smatlem 30704 qtophaus 30744 eulerpartlemgvv 31279 erdszelem10 32032 cvmlift2lem10 32144 cvmlift2lem12 32146 msubff 32297 elmpst 32303 mpstrcl 32308 elmpps 32340 dfso2 32510 fv1stcnv 32540 fv2ndcnv 32541 txpss3v 32860 dfrdg4 32933 bj-elid3 33940 bj-eldiag2 33946 bj-inftyexpitaudisj 33956 curf 34311 curunc 34315 heiborlem3 34533 xrnss3v 35069 inxpxrn 35088 dibopelvalN 37724 dibopelval2 37726 dib1dim 37746 dihopcl 37834 dih1 37867 dih1dimatlem 37910 hdmap1val 38379 pellex 38828 elnonrel 39307 fourierdlem42 41866 etransclem44 41995 ovn0lem 42279 ndmaovg 42790 aoprssdm 42808 ndmaovcl 42809 ndmaovrcl 42810 ndmaovcom 42811 ndmaovass 42812 ndmaovdistr 42813 sprsymrelfvlem 43021 sprsymrelfolem2 43024 prproropf1olem2 43035 opeliun2xp 43746 |
Copyright terms: Public domain | W3C validator |