![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elxp | GIF version |
Description: Membership in a cross product. (Contributed by NM, 4-Jul-1994.) |
Ref | Expression |
---|---|
elxp | ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xp 4407 | . . 3 ⊢ (𝐵 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} | |
2 | 1 | eleq2i 2149 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
3 | elopab 4049 | . 2 ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
4 | 2, 3 | bitri 182 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 = wceq 1285 ∃wex 1422 ∈ wcel 1434 〈cop 3425 {copab 3864 × cxp 4399 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 4000 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-opab 3866 df-xp 4407 |
This theorem is referenced by: elxp2 4419 0nelxp 4428 0nelelxp 4429 rabxp 4436 elxp3 4450 elvv 4458 elvvv 4459 0xp 4476 xpmlem 4806 elxp4 4872 elxp5 4873 dfco2a 4885 opabex3d 5827 opabex3 5828 xp1st 5871 xp2nd 5872 poxp 5932 xpsnen 6467 xpcomco 6472 xpassen 6476 nqnq0pi 6900 |
Copyright terms: Public domain | W3C validator |