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

Theorem elxp 4514
 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 4503 . . 3 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
21eleq2i 2179 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
3 elopab 4138 . 2 (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
42, 3bitri 183 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1312  ∃wex 1449   ∈ wcel 1461  ⟨cop 3494  {copab 3946   × cxp 4495 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089 This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-opab 3948  df-xp 4503 This theorem is referenced by:  elxp2  4515  0nelxp  4525  0nelelxp  4526  rabxp  4534  elxp3  4551  elvv  4559  elvvv  4560  0xp  4577  xpmlem  4915  elxp4  4982  elxp5  4983  dfco2a  4995  opabex3d  5970  opabex3  5971  xp1st  6014  xp2nd  6015  poxp  6080  xpsnen  6665  xpcomco  6670  xpassen  6674  nqnq0pi  7187  fsum2dlemstep  11088
 Copyright terms: Public domain W3C validator