Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elxp | Structured version Visualization version GIF version |
Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.) |
Ref | Expression |
---|---|
elxp | ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xp 5044 | . . 3 ⊢ (𝐵 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} | |
2 | 1 | eleq2i 2680 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
3 | elopab 4908 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | 2, 3 | bitri 263 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 〈cop 4131 {copab 4642 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-opab 4644 df-xp 5044 |
This theorem is referenced by: elxp2 5056 elxp2OLD 5057 0nelxp 5067 0nelxpOLD 5068 0nelelxp 5069 rabxp 5078 elxp3 5092 elvv 5100 elvvv 5101 0xp 5122 xpdifid 5481 dfco2a 5552 elsnxp 5594 elsnxpOLD 5595 tpres 6371 elxp4 7003 elxp5 7004 opabex3d 7037 opabex3 7038 xp1st 7089 xp2nd 7090 poxp 7176 soxp 7177 xpsnen 7929 xpcomco 7935 xpassen 7939 dfac5lem1 8829 dfac5lem4 8832 axdc4lem 9160 fsum2dlem 14343 fprod2dlem 14549 numclwlk1lem2fo 26622 dfres3 30902 elima4 30924 brcart 31209 brimg 31214 dibelval3 35454 av-numclwlk1lem2fo 41525 |
Copyright terms: Public domain | W3C validator |