Theorem opelxp 5713

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 5701	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3479	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3479	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5481	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2822	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2822	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 216	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 249	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3200	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2733	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4874	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2744	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4875	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2744	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3625	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1451	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 208	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  ⟨cop 4635   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-xp 5683

This theorem is referenced by:  opelxpi  5714  opelxp1  5719  opelxp2  5720  otelxp  5721  otel3xp  5723  brxp  5726  opthprc  5741  elxp3  5743  opeliunxp  5744  bropaex12  5768  optocl  5771  xpsspw  5810  xpiindi  5836  opelres  5988  restidsing  6053  codir  6122  qfto  6123  xpnz  6159  difxp  6164  xpdifid  6168  dfco2  6245  relssdmrnOLD  6269  ressn  6285  opelf  6753  oprab4  7495  resoprab  7526  oprssdm  7588  nssdmovg  7589  ndmovg  7590  elmpocl  7648  fo1stres  8001  fo2ndres  8002  dfoprab4  8041  opiota  8045  bropopvvv  8076  bropfvvvvlem  8077  curry1  8090  xporderlem  8113  fnwelem  8117  frpoins3xpg  8126  xpord2lem  8128  xpord2pred  8131  xpord2indlem  8133  mpoxopxprcov0  8202  mpocurryd  8254  on2recsov  8667  naddcllem  8675  brecop  8804  brecop2  8805  eceqoveq  8816  xpdom2  9067  mapunen  9146  djuss  9915  djuunxp  9916  dfac5lem2  10119  iunfo  10534  ordpipq  10937  prsrlem1  11067  opelcn  11124  opelreal  11125  elreal2  11127  swrdnznd  14592  swrd00  14594  swrdcl  14595  swrd0  14608  pfx00  14624  pfx0  14625  fsumcom2  15720  fprodcom2  15928  phimullem  16712  imasvscafn  17483  homarcl2  17985  evlfcl  18175  clatl  18461  matplusgcell  21935  iscnp2  22743  txuni2  23069  txcls  23108  txcnpi  23112  txcnp  23124  txcnmpt  23128  txdis1cn  23139  txtube  23144  hausdiag  23149  txlm  23152  tx1stc  23154  txkgen  23156  txflf  23510  tmdcn2  23593  tgphaus  23621  qustgplem  23625  fmucndlem  23796  xmeterval  23938  metustexhalf  24065  blval2  24071  bcthlem1  24841  ovolfcl  24983  ovoliunlem1  25019  mbfimaopnlem  25172  limccnp2  25409  fsumvma  26716  lgsquadlem1  26883  lgsquadlem2  26884  norec2ov  27441  dmrab  31737  xppreima2  31876  aciunf1lem  31887  f1od2  31946  smatrcl  32776  smatlem  32777  qtophaus  32816  eulerpartlemgvv  33375  erdszelem10  34191  cvmlift2lem10  34303  cvmlift2lem12  34305  msubff  34521  elmpst  34527  mpstrcl  34532  elmpps  34564  dfso2  34725  fv1stcnv  34748  fv2ndcnv  34749  txpss3v  34850  dfrdg4  34923  bj-opelrelex  36025  bj-opelidres  36042  bj-elid6  36051  bj-eldiag2  36058  bj-inftyexpitaudisj  36086  curf  36466  curunc  36470  heiborlem3  36681  xrnss3v  37242  inxpxrn  37265  dibopelvalN  40014  dibopelval2  40016  dib1dim  40036  dihopcl  40124  dih1  40157  dih1dimatlem  40200  hdmap1val  40669  pellex  41573  elnonrel  42336  mnringmulrcld  42987  fourierdlem42  44865  etransclem44  44994  ovn0lem  45281  ndmaovg  45892  aoprssdm  45910  ndmaovcl  45911  ndmaovrcl  45912  ndmaovcom  45913  ndmaovass  45914  ndmaovdistr  45915  sprsymrelfvlem  46158  sprsymrelfolem2  46161  prproropf1olem2  46172  pzriprnglem4  46808  pzriprnglem9  46813  opeliun2xp  47008  joindm2  47601  meetdm2  47603