![]() |
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 5683 | . . 3 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} | |
2 | 1 | eleq2i 2826 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
3 | elopab 5528 | . 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | 2, 3 | bitri 275 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ⟨cop 4635 {copab 5211 × cxp 5675 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-opab 5212 df-xp 5683 |
This theorem is referenced by: elxp2 5701 0nelxp 5711 0nelelxp 5712 rabxp 5725 elxp3 5743 elvv 5751 elvvv 5752 0xp 5775 dfres3 5987 xpdifid 6168 dfco2a 6246 elsnxp 6291 tpres 7202 elxp4 7913 elxp5 7914 opabex3d 7952 opabex3rd 7953 opabex3 7954 xp1st 8007 xp2nd 8008 poxp 8114 soxp 8115 xpsnen 9055 xpcomco 9062 xpassen 9066 dfac5lem1 10118 dfac5lem4 10121 axdc4lem 10450 fsum2dlem 15716 fprod2dlem 15924 numclwwlk1lem2fo 29611 satefvfmla0 34409 elima4 34747 brcart 34904 brimg 34909 dibelval3 40018 |
Copyright terms: Public domain | W3C validator |