Theorem opelxp 5661

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 5649	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3445	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3445	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5429	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2825	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2825	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 639	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3179	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2737	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4830	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2748	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4831	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2748	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3590	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1453	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  ⟨cop 4587   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-xp 5631

This theorem is referenced by:  opelxpi  5662  opelxp1  5667  opelxp2  5668  otelxp  5669  otel3xp  5671  brxp  5674  opthprc  5689  elxp3  5691  opeliunxp  5692  opeliun2xp  5693  bropaex12  5716  optoclOLD  5720  xpsspw  5759  inxp  5781  xpiindi  5785  opelres  5945  restidsing  6013  codir  6078  qfto  6079  xpnz  6118  difxp  6123  xpdifid  6127  dfco2  6204  ressn  6244  opelf  6696  oprab4  7446  resoprab  7478  oprssdm  7541  nssdmovg  7542  ndmovg  7543  elmpocl  7601  fo1stres  7961  fo2ndres  7962  dfoprab4  8001  opiota  8005  bropopvvv  8034  bropfvvvvlem  8035  curry1  8048  xporderlem  8071  fnwelem  8075  frpoins3xpg  8084  xpord2lem  8086  xpord2pred  8089  xpord2indlem  8091  mpoxopxprcov0  8161  mpocurryd  8213  on2recsov  8598  naddcllem  8606  brecop  8751  brecop2  8752  eceqoveq  8763  xpdom2  9004  mapunen  9078  djuss  9836  djuunxp  9837  dfac5lem2  10038  iunfo  10453  ordpipq  10857  prsrlem1  10987  opelcn  11044  opelreal  11045  elreal2  11047  swrdnznd  14570  swrd00  14572  swrdcl  14573  swrd0  14586  pfx00  14602  pfx0  14603  fsumcom2  15701  fprodcom2  15911  phimullem  16710  imasvscafn  17462  homarcl2  17963  evlfcl  18149  clatl  18435  pzriprnglem4  21443  pzriprnglem9  21448  matplusgcell  22381  iscnp2  23187  txuni2  23513  txcls  23552  txcnpi  23556  txcnp  23568  txcnmpt  23572  txdis1cn  23583  txtube  23588  hausdiag  23593  txlm  23596  tx1stc  23598  txkgen  23600  txflf  23954  tmdcn2  24037  tgphaus  24065  qustgplem  24069  fmucndlem  24238  xmeterval  24380  metustexhalf  24504  blval2  24510  bcthlem1  25284  ovolfcl  25427  ovoliunlem1  25463  mbfimaopnlem  25616  limccnp2  25853  fsumvma  27184  lgsquadlem1  27351  lgsquadlem2  27352  norec2ov  27939  dmrab  32553  xppreima2  32711  aciunf1lem  32722  f1od2  32779  smatrcl  33934  smatlem  33935  qtophaus  33974  eulerpartlemgvv  34514  erdszelem10  35375  cvmlift2lem10  35487  cvmlift2lem12  35489  msubff  35705  elmpst  35711  mpstrcl  35716  elmpps  35748  dfso2  35930  fv1stcnv  35952  fv2ndcnv  35953  txpss3v  36051  dfrdg4  36126  bj-opelrelex  37320  bj-opelidres  37337  bj-elid6  37346  bj-eldiag2  37353  bj-inftyexpitaudisj  37381  curf  37770  curunc  37774  heiborlem3  37985  xrnss3v  38553  ecxrn2  38580  inxpxrn  38590  dibopelvalN  41440  dibopelval2  41442  dib1dim  41462  dihopcl  41550  dih1  41583  dih1dimatlem  41626  hdmap1val  42095  aks6d1c3  42414  pellex  43113  elnonrel  43862  mnringmulrcld  44505  fourierdlem42  46429  etransclem44  46558  ovn0lem  46845  ndmaovg  47466  aoprssdm  47484  ndmaovcl  47485  ndmaovrcl  47486  ndmaovcom  47487  ndmaovass  47488  ndmaovdistr  47489  sprsymrelfvlem  47772  sprsymrelfolem2  47775  prproropf1olem2  47786  opgpgvtx  48337  iinxp  49112  coxp  49114  joindm2  49249  meetdm2  49251  swapf2fval  49546  swapf1val  49548  fuco2el  49593