Theorem elxp 4305

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

Assertion

Ref	Expression
elxp	⊢ (A ∈ (B × 𝐶) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))

Distinct variable groups:   x,y,A   x,B,y   x,𝐶,y

Proof of Theorem elxp

Step	Hyp	Ref	Expression
1		df-xp 4294	. . 3 ⊢ (B × 𝐶) = {⟨x, y⟩ ∣ (x ∈ B ∧ y ∈ 𝐶)}
2	1	eleq2i 2101	. 2 ⊢ (A ∈ (B × 𝐶) ↔ A ∈ {⟨x, y⟩ ∣ (x ∈ B ∧ y ∈ 𝐶)})
3		elopab 3986	. 2 ⊢ (A ∈ {⟨x, y⟩ ∣ (x ∈ B ∧ y ∈ 𝐶)} ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))
4	2, 3	bitri 173	1 ⊢ (A ∈ (B × 𝐶) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))

Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ⟨cop 3370  {copab 3808   × cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by:  elxp2  4306  0nelxp  4315  0nelelxp  4316  rabxp  4323  elxp3  4337  elvv  4345  elvvv  4346  0xp  4363  xpmlem  4687  elxp4  4751  elxp5  4752  dfco2a  4764  opabex3d  5690  opabex3  5691  xp1st  5734  xp2nd  5735  poxp  5794  xpsnen  6231  xpcomco  6236  xpassen  6240  nqnq0pi  6421