ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elxp GIF version

Theorem elxp 4418
Description: Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elxp (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem elxp
StepHypRef Expression
1 df-xp 4407 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2149 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 4049 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 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