| 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 460 | . . 3 ⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
| 2 | 1 | 2exbii 1848 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
| 3 | elxp 5675 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
| 4 | r2ex 3179 | . 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ∃wrex 3059 〈cop 4605 × cxp 5650 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2706 ax-sep 5264 ax-nul 5274 ax-pr 5400 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2713 df-cleq 2726 df-clel 2808 df-ral 3051 df-rex 3060 df-v 3459 df-dif 3927 df-un 3929 df-ss 3941 df-nul 4307 df-if 4499 df-sn 4600 df-pr 4602 df-op 4606 df-opab 5180 df-xp 5658 |
| This theorem is referenced by: opelxp 5688 xpiundi 5723 xpiundir 5724 ssrel2 5762 reuop 6280 el2xptp 8029 f1o2ndf1 8116 frpoins3xpg 8134 poxp2 8137 xpord2pred 8139 sexp2 8140 xpdom2 9076 tskxpss 10779 nqereu 10936 elreal 11138 xpsmnd0 18743 efgmnvl 19682 frgpuptinv 19739 frgpup3lem 19745 xpsring1d 20280 pzriprnglem3 21431 pzriprnglem8 21436 pzriprnglem10 21438 ucnima 24206 ltgseg 28509 suppovss 32592 elrlocbasi 33198 qtophaus 33796 esum2dlem 34052 bj-mpomptALT 37066 fourierdlem42 46114 gpgvtxel 47958 |
| Copyright terms: Public domain | W3C validator |