Theorem opelxp 5696

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 5684	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3458	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5461	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2850	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2850	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 649	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3206	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2762	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4837	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2773	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4838	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2773	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3593	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1478	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   = wceq 1569   ∈ wcel 2142  ∃wrex 3088  ⟨cop 4594   × cxp 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-opab 5173  df-xp 5666

This theorem is used by:  opelxpi  5697  opelxp1  5702  opelxp2  5703  otelxp  5704  otel3xp  5706  brxp  5709  opthprc  5724  elxp3  5726  opeliunxp  5727  opeliun2xp  5728  bropaex12  5751  optoclOLD  5755  xpsspw  5795  inxp  5817  xpiindi  5820  opelres  5983  restidsing  6054  codir  6119  qfto  6120  xpnz  6155  difxp  6160  xpdifid  6164  xpdifcnvepel  6165  dfco2  6245  ressn  6286  opelf  6739  oprab4  7498  resoprab  7530  oprssdm  7593  nssdmovg  7594  ndmovg  7595  elmpocl  7653  fo1stres  8010  fo2ndres  8011  dfoprab4  8050  opiota  8054  bropopvvv  8083  bropfvvvvlem  8084  curry1  8097  xporderlem  8121  fnwelem  8125  frpoins3xpg  8134  xpord2lem  8136  xpord2pred  8139  xpord2indlem  8141  mpoxopxprcov0  8211  mpocurryd  8263  on2recsov  8652  naddcllem  8660  brecop  8806  brecop2  8807  eceqoveq  8818  xpdom2  9058  mapunen  9132  djuss  9913  djuunxp  9914  dfac5lem2  10115  iunfo  10529  ordpipq  10933  prsrlem1  11063  opelcn  11120  opelreal  11121  elreal2  11123  swrdnznd  14687  swrd00  14689  swrdcl  14690  swrd0  14703  pfx00  14719  pfx0  14720  fsumcom2  15832  fprodcom2  16045  phimullem  16844  imasvscafn  17597  homarcl2  18098  evlfcl  18284  clatl  18570  pzriprnglem4  21645  pzriprnglem9  21650  matplusgcell  22601  iscnp2  23407  txuni2  23733  txcls  23772  txcnpi  23776  txcnp  23788  txcnmpt  23792  txdis1cn  23803  txtube  23808  hausdiag  23813  txlm  23816  tx1stc  23818  txkgen  23820  txflf  24174  tmdcn2  24257  tgphaus  24285  qustgplem  24289  fmucndlem  24458  xmeterval  24600  metustexhalf  24724  blval2  24730  bcthlem1  25494  ovolfcl  25636  ovoliunlem1  25672  mbfimaopnlem  25825  limccnp2  26062  fsumvma  27388  lgsquadlem1  27555  lgsquadlem2  27556  norec2ov  28161  dmrab  32854  xppreima2  33007  aciunf1lem  33018  f1od2  33075  smatrcl  34195  smatlem  34196  qtophaus  34235  eulerpartlemgvv  34775  erdszelem10  35700  cvmlift2lem10  35812  cvmlift2lem12  35814  msubff  36030  elmpst  36036  mpstrcl  36041  elmpps  36073  dfso2  36255  fv1stcnv  36277  fv2ndcnv  36278  txpss3v  36376  dfrdg4  36451  bj-opelrelex  37816  bj-opelidres  37833  bj-elid6  37842  bj-eldiag2  37849  bj-inftyexpitaudisj  37877  curf  38277  curunc  38281  heiborlem3  38492  xrnss3v  39058  ecxrn2  39085  inxpxrn  39095  dibopelvalN  41945  dibopelval2  41947  dib1dim  41967  dihopcl  42055  dih1  42088  dih1dimatlem  42131  hdmap1val  42600  aks6d1c3  42918  pellex  43590  elnonrel  44339  mnringmulrcld  44980  fourierdlem42  46891  etransclem44  47020  ovn0lem  47307  ndmaovg  47949  aoprssdm  47967  ndmaovcl  47968  ndmaovrcl  47969  ndmaovcom  47970  ndmaovass  47971  ndmaovdistr  47972  sprsymrelfvlem  48267  sprsymrelfolem2  48270  prproropf1olem2  48281  opgpgvtx  48848  iinxp  49637  coxp  49639  joindm2  49774  meetdm2  49776  swapf2fval  50071  swapf1val  50073  fuco2el  50118