| 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 1849 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
| 3 | elxp 5664 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
| 4 | r2ex 3175 | . 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∃wrex 3054 〈cop 4598 × cxp 5639 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-ral 3046 df-rex 3055 df-v 3452 df-dif 3920 df-un 3922 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-opab 5173 df-xp 5647 |
| This theorem is referenced by: opelxp 5677 xpiundi 5712 xpiundir 5713 ssrel2 5751 reuop 6269 el2xptp 8017 f1o2ndf1 8104 frpoins3xpg 8122 poxp2 8125 xpord2pred 8127 sexp2 8128 xpdom2 9041 tskxpss 10732 nqereu 10889 elreal 11091 xpsmnd0 18712 efgmnvl 19651 frgpuptinv 19708 frgpup3lem 19714 xpsring1d 20249 pzriprnglem3 21400 pzriprnglem8 21405 pzriprnglem10 21407 ucnima 24175 ltgseg 28530 suppovss 32611 elrlocbasi 33224 qtophaus 33833 esum2dlem 34089 bj-mpomptALT 37114 fourierdlem42 46154 gpgvtxel 48042 |
| Copyright terms: Public domain | W3C validator |