Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elxp2 Structured version   Visualization version   GIF version

Theorem elxp2 5572
 Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004.) (Proof shortened by JJ, 13-Aug-2021.)
Assertion
Ref Expression
elxp2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem elxp2
StepHypRef Expression
1 ancom 463 . . 3 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
212exbii 1843 . 2 (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥𝑦((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
3 elxp 5571 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
4 r2ex 3301 . 2 (∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦((𝑥𝐵𝑦𝐶) ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
52, 3, 43bitr4i 305 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108  ∃wrex 3137  ⟨cop 4565   × cxp 5546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-opab 5120  df-xp 5554 This theorem is referenced by:  opelxp  5584  xpiundi  5615  xpiundir  5616  ssrel2  5652  reuop  6137  el2xptp  7727  f1o2ndf1  7810  xpdom2  8604  tskxpss  10186  nqereu  10343  elreal  10545  efgmnvl  18832  frgpuptinv  18889  frgpup3lem  18895  ucnima  22882  ltgseg  26374  suppovss  30418  qtophaus  31093  esum2dlem  31344  bj-mpomptALT  34403  fourierdlem42  42424
 Copyright terms: Public domain W3C validator