Theorem opelxp 5667

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 5655	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3448	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3448	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5435	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2816	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2816	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3177	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2729	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4833	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2740	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4834	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3598	. . . 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 1540   ∈ wcel 2109  ∃wrex 3053  ⟨cop 4591   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637

This theorem is referenced by:  opelxpi  5668  opelxp1  5673  opelxp2  5674  otelxp  5675  otel3xp  5677  brxp  5680  opthprc  5695  elxp3  5697  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  optocl  5725  xpsspw  5763  inxp  5785  xpiindi  5789  opelres  5945  restidsing  6013  codir  6081  qfto  6082  xpnz  6120  difxp  6125  xpdifid  6129  dfco2  6206  relssdmrnOLD  6230  ressn  6246  opelf  6703  oprab4  7455  resoprab  7487  oprssdm  7550  nssdmovg  7551  ndmovg  7552  elmpocl  7610  fo1stres  7973  fo2ndres  7974  dfoprab4  8013  opiota  8017  bropopvvv  8046  bropfvvvvlem  8047  curry1  8060  xporderlem  8083  fnwelem  8087  frpoins3xpg  8096  xpord2lem  8098  xpord2pred  8101  xpord2indlem  8103  mpoxopxprcov0  8173  mpocurryd  8225  on2recsov  8609  naddcllem  8617  brecop  8760  brecop2  8761  eceqoveq  8772  xpdom2  9013  mapunen  9087  djuss  9849  djuunxp  9850  dfac5lem2  10053  iunfo  10468  ordpipq  10871  prsrlem1  11001  opelcn  11058  opelreal  11059  elreal2  11061  swrdnznd  14583  swrd00  14585  swrdcl  14586  swrd0  14599  pfx00  14615  pfx0  14616  fsumcom2  15716  fprodcom2  15926  phimullem  16725  imasvscafn  17476  homarcl2  17977  evlfcl  18163  clatl  18449  pzriprnglem4  21426  pzriprnglem9  21431  matplusgcell  22353  iscnp2  23159  txuni2  23485  txcls  23524  txcnpi  23528  txcnp  23540  txcnmpt  23544  txdis1cn  23555  txtube  23560  hausdiag  23565  txlm  23568  tx1stc  23570  txkgen  23572  txflf  23926  tmdcn2  24009  tgphaus  24037  qustgplem  24041  fmucndlem  24211  xmeterval  24353  metustexhalf  24477  blval2  24483  bcthlem1  25257  ovolfcl  25400  ovoliunlem1  25436  mbfimaopnlem  25589  limccnp2  25826  fsumvma  27157  lgsquadlem1  27324  lgsquadlem2  27325  norec2ov  27904  dmrab  32476  xppreima2  32625  aciunf1lem  32636  f1od2  32694  smatrcl  33779  smatlem  33780  qtophaus  33819  eulerpartlemgvv  34360  erdszelem10  35180  cvmlift2lem10  35292  cvmlift2lem12  35294  msubff  35510  elmpst  35516  mpstrcl  35521  elmpps  35553  dfso2  35735  fv1stcnv  35757  fv2ndcnv  35758  txpss3v  35859  dfrdg4  35932  bj-opelrelex  37125  bj-opelidres  37142  bj-elid6  37151  bj-eldiag2  37158  bj-inftyexpitaudisj  37186  curf  37585  curunc  37589  heiborlem3  37800  xrnss3v  38347  inxpxrn  38374  dibopelvalN  41130  dibopelval2  41132  dib1dim  41152  dihopcl  41240  dih1  41273  dih1dimatlem  41316  hdmap1val  41785  aks6d1c3  42104  pellex  42816  elnonrel  43567  mnringmulrcld  44210  fourierdlem42  46140  etransclem44  46269  ovn0lem  46556  ndmaovg  47178  aoprssdm  47196  ndmaovcl  47197  ndmaovrcl  47198  ndmaovcom  47199  ndmaovass  47200  ndmaovdistr  47201  sprsymrelfvlem  47484  sprsymrelfolem2  47487  prproropf1olem2  47498  opgpgvtx  48039  iinxp  48812  coxp  48814  joindm2  48949  meetdm2  48951  swapf2fval  49247  swapf1val  49249  fuco2el  49294