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 3434	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3434	. . . . . . 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 3180	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2737	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4817	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2748	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4818	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2748	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3578	. . . 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 3062  ⟨cop 4574   × 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 5232  ax-pr 5371

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  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  7447  resoprab  7479  oprssdm  7542  nssdmovg  7543  ndmovg  7544  elmpocl  7602  fo1stres  7962  fo2ndres  7963  dfoprab4  8002  opiota  8006  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  9838  djuunxp  9839  dfac5lem2  10040  iunfo  10455  ordpipq  10859  prsrlem1  10989  opelcn  11046  opelreal  11047  elreal2  11049  swrdnznd  14599  swrd00  14601  swrdcl  14602  swrd0  14615  pfx00  14631  pfx0  14632  fsumcom2  15730  fprodcom2  15943  phimullem  16743  imasvscafn  17495  homarcl2  17996  evlfcl  18182  clatl  18468  pzriprnglem4  21477  pzriprnglem9  21482  matplusgcell  22411  iscnp2  23217  txuni2  23543  txcls  23582  txcnpi  23586  txcnp  23598  txcnmpt  23602  txdis1cn  23613  txtube  23618  hausdiag  23623  txlm  23626  tx1stc  23628  txkgen  23630  txflf  23984  tmdcn2  24067  tgphaus  24095  qustgplem  24099  fmucndlem  24268  xmeterval  24410  metustexhalf  24534  blval2  24540  bcthlem1  25304  ovolfcl  25446  ovoliunlem1  25482  mbfimaopnlem  25635  limccnp2  25872  fsumvma  27193  lgsquadlem1  27360  lgsquadlem2  27361  norec2ov  27966  dmrab  32584  xppreima2  32742  aciunf1lem  32753  f1od2  32810  smatrcl  33959  smatlem  33960  qtophaus  33999  eulerpartlemgvv  34539  erdszelem10  35401  cvmlift2lem10  35513  cvmlift2lem12  35515  msubff  35731  elmpst  35737  mpstrcl  35742  elmpps  35774  dfso2  35956  fv1stcnv  35978  fv2ndcnv  35979  txpss3v  36077  dfrdg4  36152  bj-opelrelex  37477  bj-opelidres  37494  bj-elid6  37503  bj-eldiag2  37510  bj-inftyexpitaudisj  37538  curf  37936  curunc  37940  heiborlem3  38151  xrnss3v  38719  ecxrn2  38746  inxpxrn  38756  dibopelvalN  41606  dibopelval2  41608  dib1dim  41628  dihopcl  41716  dih1  41749  dih1dimatlem  41792  hdmap1val  42261  aks6d1c3  42579  pellex  43284  elnonrel  44033  mnringmulrcld  44676  fourierdlem42  46598  etransclem44  46727  ovn0lem  47014  ndmaovg  47647  aoprssdm  47665  ndmaovcl  47666  ndmaovrcl  47667  ndmaovcom  47668  ndmaovass  47669  ndmaovdistr  47670  sprsymrelfvlem  47965  sprsymrelfolem2  47968  prproropf1olem2  47979  opgpgvtx  48546  iinxp  49321  coxp  49323  joindm2  49458  meetdm2  49460  swapf2fval  49755  swapf1val  49757  fuco2el  49802