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 5554 | . . 3 ⊢ (𝐵 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} | |
2 | 1 | eleq2i 2829 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
3 | elopab 5405 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | 2, 3 | bitri 278 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1543 ∃wex 1787 ∈ wcel 2110 〈cop 4544 {copab 5112 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3407 df-dif 3866 df-un 3868 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-opab 5113 df-xp 5554 |
This theorem is referenced by: elxp2 5572 0nelxp 5582 0nelelxp 5583 rabxp 5594 elxp3 5612 elvv 5620 elvvv 5621 0xp 5643 dfres3 5853 xpdifid 6028 dfco2a 6107 elsnxp 6151 tpres 7013 elxp4 7697 elxp5 7698 opabex3d 7735 opabex3rd 7736 opabex3 7737 xp1st 7790 xp2nd 7791 poxp 7892 soxp 7893 xpsnen 8726 xpcomco 8732 xpassen 8736 dfac5lem1 9734 dfac5lem4 9737 axdc4lem 10066 fsum2dlem 15331 fprod2dlem 15539 numclwwlk1lem2fo 28438 satefvfmla0 33090 elima4 33466 brcart 33968 brimg 33973 dibelval3 38896 |
Copyright terms: Public domain | W3C validator |