![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elxp2 | Structured version Visualization version GIF version |
Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004.) (Proof shortened by JJ, 13-Aug-2021.) |
Ref | Expression |
---|---|
elxp2 | ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 454 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
2 | 1 | 2exbii 1950 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
3 | elxp 5366 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | r2ex 3272 | . 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
5 | 2, 3, 4 | 3bitr4i 295 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 = wceq 1658 ∃wex 1880 ∈ wcel 2166 ∃wrex 3119 〈cop 4404 × cxp 5341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-opab 4937 df-xp 5349 |
This theorem is referenced by: opelxp 5379 xpiundi 5407 xpiundir 5408 ssrel2 5445 el2xptp 7474 f1o2ndf1 7550 xpdom2 8325 tskxpss 9910 nqereu 10067 elreal 10269 efgmnvl 18479 frgpuptinv 18538 frgpup3lem 18544 ucnima 22456 ltgseg 25909 qtophaus 30449 esum2dlem 30700 bj-mpt2mptALT 33596 fourierdlem42 41161 |
Copyright terms: Public domain | W3C validator |