![]() |
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 1843 | . 2 ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
3 | elxp 5689 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | r2ex 3187 | . 2 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ∧ 𝐴 = 〈𝑥, 𝑦〉)) | |
5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = 〈𝑥, 𝑦〉) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∃wrex 3062 〈cop 4626 × cxp 5664 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ral 3054 df-rex 3063 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-opab 5201 df-xp 5672 |
This theorem is referenced by: opelxp 5702 xpiundi 5736 xpiundir 5737 ssrel2 5775 reuop 6282 el2xptp 8014 f1o2ndf1 8102 frpoins3xpg 8120 poxp2 8123 xpord2pred 8125 sexp2 8126 xpdom2 9063 tskxpss 10763 nqereu 10920 elreal 11122 xpsmnd0 18698 efgmnvl 19624 frgpuptinv 19681 frgpup3lem 19687 xpsring1d 20222 pzriprnglem3 21338 pzriprnglem8 21343 pzriprnglem10 21345 ucnima 24108 ltgseg 28316 suppovss 32375 qtophaus 33305 esum2dlem 33579 bj-mpomptALT 36490 fourierdlem42 45350 |
Copyright terms: Public domain | W3C validator |