Theorem opelxp 5660

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 5648	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3444	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3444	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5428	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2824	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2824	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3178	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4829	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4830	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3589	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1452	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  ⟨cop 4586   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-xp 5630

This theorem is referenced by:  opelxpi  5661  opelxp1  5666  opelxp2  5667  otelxp  5668  otel3xp  5670  brxp  5673  opthprc  5688  elxp3  5690  opeliunxp  5691  opeliun2xp  5692  bropaex12  5715  optoclOLD  5719  xpsspw  5758  inxp  5780  xpiindi  5784  opelres  5944  restidsing  6012  codir  6077  qfto  6078  xpnz  6117  difxp  6122  xpdifid  6126  dfco2  6203  ressn  6243  opelf  6695  oprab4  7444  resoprab  7476  oprssdm  7539  nssdmovg  7540  ndmovg  7541  elmpocl  7599  fo1stres  7959  fo2ndres  7960  dfoprab4  7999  opiota  8003  bropopvvv  8032  bropfvvvvlem  8033  curry1  8046  xporderlem  8069  fnwelem  8073  frpoins3xpg  8082  xpord2lem  8084  xpord2pred  8087  xpord2indlem  8089  mpoxopxprcov0  8159  mpocurryd  8211  on2recsov  8596  naddcllem  8604  brecop  8747  brecop2  8748  eceqoveq  8759  xpdom2  9000  mapunen  9074  djuss  9832  djuunxp  9833  dfac5lem2  10034  iunfo  10449  ordpipq  10853  prsrlem1  10983  opelcn  11040  opelreal  11041  elreal2  11043  swrdnznd  14566  swrd00  14568  swrdcl  14569  swrd0  14582  pfx00  14598  pfx0  14599  fsumcom2  15697  fprodcom2  15907  phimullem  16706  imasvscafn  17458  homarcl2  17959  evlfcl  18145  clatl  18431  pzriprnglem4  21439  pzriprnglem9  21444  matplusgcell  22377  iscnp2  23183  txuni2  23509  txcls  23548  txcnpi  23552  txcnp  23564  txcnmpt  23568  txdis1cn  23579  txtube  23584  hausdiag  23589  txlm  23592  tx1stc  23594  txkgen  23596  txflf  23950  tmdcn2  24033  tgphaus  24061  qustgplem  24065  fmucndlem  24234  xmeterval  24376  metustexhalf  24500  blval2  24506  bcthlem1  25280  ovolfcl  25423  ovoliunlem1  25459  mbfimaopnlem  25612  limccnp2  25849  fsumvma  27180  lgsquadlem1  27347  lgsquadlem2  27348  norec2ov  27953  dmrab  32571  xppreima2  32729  aciunf1lem  32740  f1od2  32798  smatrcl  33953  smatlem  33954  qtophaus  33993  eulerpartlemgvv  34533  erdszelem10  35394  cvmlift2lem10  35506  cvmlift2lem12  35508  msubff  35724  elmpst  35730  mpstrcl  35735  elmpps  35767  dfso2  35949  fv1stcnv  35971  fv2ndcnv  35972  txpss3v  36070  dfrdg4  36145  bj-opelrelex  37349  bj-opelidres  37366  bj-elid6  37375  bj-eldiag2  37382  bj-inftyexpitaudisj  37410  curf  37799  curunc  37803  heiborlem3  38014  xrnss3v  38576  ecxrn2  38603  inxpxrn  38613  dibopelvalN  41413  dibopelval2  41415  dib1dim  41435  dihopcl  41523  dih1  41556  dih1dimatlem  41599  hdmap1val  42068  aks6d1c3  42387  pellex  43087  elnonrel  43836  mnringmulrcld  44479  fourierdlem42  46403  etransclem44  46532  ovn0lem  46819  ndmaovg  47440  aoprssdm  47458  ndmaovcl  47459  ndmaovrcl  47460  ndmaovcom  47461  ndmaovass  47462  ndmaovdistr  47463  sprsymrelfvlem  47746  sprsymrelfolem2  47749  prproropf1olem2  47760  opgpgvtx  48311  iinxp  49086  coxp  49088  joindm2  49223  meetdm2  49225  swapf2fval  49520  swapf1val  49522  fuco2el  49567