Theorem opelxp 5572

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opelxp	⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem opelxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5560	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3402	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3402	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5349	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2818	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2818	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 639	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3201	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4770	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4771	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3539	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1452	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∃wrex 3052  ⟨cop 4533   × cxp 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-opab 5102  df-xp 5542

This theorem is referenced by:  opelxpi  5573  opelxp1  5577  opelxp2  5578  otel3xp  5580  brxp  5583  opthprc  5598  elxp3  5600  opeliunxp  5601  bropaex12  5624  optocl  5627  xpsspw  5664  xpiindi  5689  opelres  5842  restidsing  5907  codir  5965  qfto  5966  xpnz  6002  difxp  6007  xpdifid  6011  dfco2  6089  relssdmrn  6112  ressn  6128  opelf  6558  oprab4  7275  resoprab  7306  oprssdm  7367  nssdmovg  7368  ndmovg  7369  elmpocl  7425  fo1stres  7765  fo2ndres  7766  dfoprab4  7803  opiota  7807  bropopvvv  7836  bropfvvvvlem  7837  curry1  7850  xporderlem  7872  fnwelem  7876  mpoxopxprcov0  7937  mpocurryd  7989  brecop  8470  brecop2  8471  eceqoveq  8482  xpdom2  8718  mapunen  8793  djuss  9501  djuunxp  9502  dfac5lem2  9703  iunfo  10118  ordpipq  10521  prsrlem1  10651  opelcn  10708  opelreal  10709  elreal2  10711  swrdnznd  14172  swrd00  14174  swrdcl  14175  swrd0  14188  pfx00  14204  pfx0  14205  fsumcom2  15301  fprodcom2  15509  phimullem  16295  imasvscafn  16996  homarcl2  17495  evlfcl  17684  clatl  17968  matplusgcell  21284  iscnp2  22090  txuni2  22416  txcls  22455  txcnpi  22459  txcnp  22471  txcnmpt  22475  txdis1cn  22486  txtube  22491  hausdiag  22496  txlm  22499  tx1stc  22501  txkgen  22503  txflf  22857  tmdcn2  22940  tgphaus  22968  qustgplem  22972  fmucndlem  23142  xmeterval  23284  metustexhalf  23408  blval2  23414  bcthlem1  24175  ovolfcl  24317  ovoliunlem1  24353  mbfimaopnlem  24506  limccnp2  24743  fsumvma  26048  lgsquadlem1  26215  lgsquadlem2  26216  dmrab  30517  xppreima2  30661  aciunf1lem  30673  f1od2  30730  smatrcl  31414  smatlem  31415  qtophaus  31454  eulerpartlemgvv  32009  erdszelem10  32829  cvmlift2lem10  32941  cvmlift2lem12  32943  msubff  33159  elmpst  33165  mpstrcl  33170  elmpps  33202  ot2elxp  33349  dfso2  33391  fv1stcnv  33421  fv2ndcnv  33422  frpoins3xpg  33457  xpord2lem  33469  xpord2pred  33472  xpord2ind  33474  xpord3pred  33478  on2recsov  33513  naddcllem  33517  norec2ov  33800  txpss3v  33866  dfrdg4  33939  bj-opelrelex  34999  bj-opelidres  35016  bj-elid6  35025  bj-eldiag2  35032  bj-inftyexpitaudisj  35060  curf  35441  curunc  35445  heiborlem3  35657  xrnss3v  36188  inxpxrn  36207  dibopelvalN  38843  dibopelval2  38845  dib1dim  38865  dihopcl  38953  dih1  38986  dih1dimatlem  39029  hdmap1val  39498  pellex  40301  elnonrel  40810  mnringmulrcld  41460  fourierdlem42  43308  etransclem44  43437  ovn0lem  43721  ndmaovg  44291  aoprssdm  44309  ndmaovcl  44310  ndmaovrcl  44311  ndmaovcom  44312  ndmaovass  44313  ndmaovdistr  44314  sprsymrelfvlem  44558  sprsymrelfolem2  44561  prproropf1olem2  44572  opeliun2xp  45284  joindm2  45878  meetdm2  45880