Theorem elxp 5661

Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
elxp	⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem elxp

Step	Hyp	Ref	Expression
1		df-xp 5644	. . 3 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ 𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
3		elopab 5487	. 2 ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4	2, 3	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ⟨cop 4595  {copab 5169   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644

This theorem is referenced by:  elxp2  5662  0nelxp  5672  0nelelxp  5673  rabxp  5686  elxp3  5704  elvv  5713  elvvv  5714  0xp  5737  dfres3  5955  xpdifid  6141  dfco2a  6219  elsnxp  6264  tpres  7175  elxp4  7898  elxp5  7899  opabex3d  7944  opabex3rd  7945  opabex3  7946  xp1st  8000  xp2nd  8001  poxp  8107  soxp  8108  xpsnen  9025  xpcomco  9031  xpassen  9035  dfac5lem1  10076  dfac5lem4  10079  dfac5lem4OLD  10081  axdc4lem  10408  fsum2dlem  15736  fprod2dlem  15946  numclwwlk1lem2fo  30287  satefvfmla0  35405  elima4  35763  brcart  35920  brimg  35925  dibelval3  41141