Theorem opelxp 5697

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 5685	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3459	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3459	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5462	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2851	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2851	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 649	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3207	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2763	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4838	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2774	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4839	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2774	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3594	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1479	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  ⟨cop 4595   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174  df-xp 5667

This theorem is referenced by:  opelxpi  5698  opelxp1  5703  opelxp2  5704  otelxp  5705  otel3xp  5707  brxp  5710  opthprc  5725  elxp3  5727  opeliunxp  5728  opeliun2xp  5729  bropaex12  5752  optoclOLD  5756  xpsspw  5796  inxp  5818  xpiindi  5821  opelres  5984  restidsing  6055  codir  6120  qfto  6121  xpnz  6156  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  dfco2  6246  ressn  6286  opelf  6739  oprab4  7496  resoprab  7528  oprssdm  7591  nssdmovg  7592  ndmovg  7593  elmpocl  7651  fo1stres  8008  fo2ndres  8009  dfoprab4  8048  opiota  8052  bropopvvv  8081  bropfvvvvlem  8082  curry1  8095  xporderlem  8119  fnwelem  8123  frpoins3xpg  8132  xpord2lem  8134  xpord2pred  8137  xpord2indlem  8139  mpoxopxprcov0  8209  mpocurryd  8261  on2recsov  8650  naddcllem  8658  brecop  8804  brecop2  8805  eceqoveq  8816  xpdom2  9056  mapunen  9130  djuss  9902  djuunxp  9903  dfac5lem2  10104  iunfo  10518  ordpipq  10922  prsrlem1  11052  opelcn  11109  opelreal  11110  elreal2  11112  swrdnznd  14676  swrd00  14678  swrdcl  14679  swrd0  14692  pfx00  14708  pfx0  14709  fsumcom2  15821  fprodcom2  16034  phimullem  16833  imasvscafn  17586  homarcl2  18087  evlfcl  18273  clatl  18559  pzriprnglem4  21634  pzriprnglem9  21639  matplusgcell  22590  iscnp2  23396  txuni2  23722  txcls  23761  txcnpi  23765  txcnp  23777  txcnmpt  23781  txdis1cn  23792  txtube  23797  hausdiag  23802  txlm  23805  tx1stc  23807  txkgen  23809  txflf  24163  tmdcn2  24246  tgphaus  24274  qustgplem  24278  fmucndlem  24447  xmeterval  24589  metustexhalf  24713  blval2  24719  bcthlem1  25483  ovolfcl  25625  ovoliunlem1  25661  mbfimaopnlem  25814  limccnp2  26051  fsumvma  27377  lgsquadlem1  27544  lgsquadlem2  27545  norec2ov  28150  dmrab  32843  xppreima2  32996  aciunf1lem  33007  f1od2  33064  smatrcl  34186  smatlem  34187  qtophaus  34226  eulerpartlemgvv  34766  erdszelem10  35692  cvmlift2lem10  35804  cvmlift2lem12  35806  msubff  36022  elmpst  36028  mpstrcl  36033  elmpps  36065  dfso2  36247  fv1stcnv  36269  fv2ndcnv  36270  txpss3v  36368  dfrdg4  36443  bj-opelrelex  37808  bj-opelidres  37825  bj-elid6  37834  bj-eldiag2  37841  bj-inftyexpitaudisj  37869  curf  38269  curunc  38273  heiborlem3  38484  xrnss3v  39050  ecxrn2  39077  inxpxrn  39087  dibopelvalN  41937  dibopelval2  41939  dib1dim  41959  dihopcl  42047  dih1  42080  dih1dimatlem  42123  hdmap1val  42592  aks6d1c3  42910  pellex  43582  elnonrel  44331  mnringmulrcld  44972  fourierdlem42  46883  etransclem44  47012  ovn0lem  47299  ndmaovg  47941  aoprssdm  47959  ndmaovcl  47960  ndmaovrcl  47961  ndmaovcom  47962  ndmaovass  47963  ndmaovdistr  47964  sprsymrelfvlem  48259  sprsymrelfolem2  48262  prproropf1olem2  48273  opgpgvtx  48840  iinxp  49629  coxp  49631  joindm2  49766  meetdm2  49768  swapf2fval  50063  swapf1val  50065  fuco2el  50110