Theorem opelxp 5180

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 5166	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3234	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3234	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 4978	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2718	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2718	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 935	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 207	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 240	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3065	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2651	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4433	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2661	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4434	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2661	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3355	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1453	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 199	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 264	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∃wrex 2942  ⟨cop 4216   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-opab 4746  df-xp 5149

This theorem is referenced by:  brxp  5181  opelxpi  5182  opelxp1  5184  opelxp2  5185  otel3xp  5187  opthprc  5201  elxp3  5203  opeliunxp  5204  bropaex12  5226  optocl  5229  xpsspw  5266  xpiindi  5290  opelresg  5434  opelresOLD  5438  restidsing  5493  restidsingOLD  5494  codir  5551  qfto  5552  xpnz  5588  difxp  5593  xpdifid  5597  ssrnres  5607  dfco2  5672  relssdmrn  5694  ressn  5709  elsnxpOLD  5716  opelf  6103  oprab4  6768  resoprab  6798  oprssdm  6857  nssdmovg  6858  ndmovg  6859  elmpt2cl  6918  resiexg  7144  fo1stres  7236  fo2ndres  7237  el2xptp0  7256  dfoprab4  7269  opiota  7273  bropopvvv  7300  bropfvvvvlem  7301  curry1  7314  curry2  7317  xporderlem  7333  fnwelem  7337  mpt2xopxprcov0  7388  mpt2curryd  7440  brecop  7883  brecop2  7884  eceqoveq  7895  xpdom2  8096  mapunen  8170  dfac5lem2  8985  iunfo  9399  ordpipq  9802  prsrlem1  9931  opelcn  9988  opelreal  9989  elreal2  9991  swrd00  13463  swrdcl  13464  swrd0  13480  fsumcom2  14549  fsumcom2OLD  14550  fprodcom2  14758  fprodcom2OLD  14759  phimullem  15531  imasvscafn  16244  brcic  16505  homarcl2  16732  evlfcl  16909  clatl  17163  matplusgcell  20287  mdetrlin  20456  iscnp2  21091  txuni2  21416  txcls  21455  txcnpi  21459  txcnp  21471  txcnmpt  21475  txdis1cn  21486  txtube  21491  hausdiag  21496  txlm  21499  tx1stc  21501  txkgen  21503  txflf  21857  tmdcn2  21940  tgphaus  21967  qustgplem  21971  fmucndlem  22142  xmeterval  22284  metustexhalf  22408  blval2  22414  metuel2  22417  bcthlem1  23167  ovolfcl  23281  ovoliunlem1  23316  ovolshftlem1  23323  mbfimaopnlem  23467  limccnp2  23701  cxpcn3  24534  fsumvma  24983  lgsquadlem1  25150  lgsquadlem2  25151  ofresid  29572  xppreima2  29578  aciunf1lem  29590  f1od2  29627  smatrcl  29990  smatlem  29991  qtophaus  30031  eulerpartlemgvv  30566  erdszelem10  31308  cvmlift2lem10  31420  cvmlift2lem12  31422  msubff  31553  elmpst  31559  mpstrcl  31564  elmpps  31596  dfso2  31770  fv1stcnv  31804  fv2ndcnv  31805  txpss3v  32110  pprodss4v  32116  dfrdg4  32183  bj-elid3  33217  bj-eldiag2  33222  curf  33517  curunc  33521  heiborlem3  33742  opelresALTV  34172  xrnss3v  34274  inxpxrn  34293  dibopelvalN  36749  dibopelval2  36751  dib1dim  36771  dihopcl  36859  dih1  36892  dih1dimatlem  36935  hdmap1val  37405  pellex  37716  elnonrel  38208  fourierdlem42  40684  etransclem44  40813  ovn0lem  41100  ndmaovg  41585  aoprssdm  41603  ndmaovcl  41604  ndmaovrcl  41605  ndmaovcom  41606  ndmaovass  41607  ndmaovdistr  41608  pfx00  41709  pfx0  41710  sprsymrelfvlem  42065  sprsymrelfolem2  42068  opeliun2xp  42436