Theorem opelxp 5698

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 5686	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3467	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3467	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5463	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2857	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2857	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 649	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3213	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2769	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4842	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2780	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4843	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2780	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3603	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1476	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  ⟨cop 4600   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178  df-xp 5668

This theorem is referenced by:  opelxpi  5699  opelxp1  5704  opelxp2  5705  otelxp  5706  otel3xp  5708  brxp  5711  opthprc  5726  elxp3  5728  opeliunxp  5729  opeliun2xp  5730  bropaex12  5753  optoclOLD  5757  xpsspw  5797  inxp  5819  xpiindi  5822  opelres  5985  restidsing  6056  codir  6121  qfto  6122  xpnz  6157  difxp  6162  xpdifid  6166  xpdifcnvepel  6167  dfco2  6247  ressn  6287  opelf  6740  oprab4  7497  resoprab  7529  oprssdm  7592  nssdmovg  7593  ndmovg  7594  elmpocl  7652  fo1stres  8012  fo2ndres  8013  dfoprab4  8052  opiota  8056  bropopvvv  8085  bropfvvvvlem  8086  curry1  8099  xporderlem  8123  fnwelem  8127  frpoins3xpg  8136  xpord2lem  8138  xpord2pred  8141  xpord2indlem  8143  mpoxopxprcov0  8213  mpocurryd  8265  on2recsov  8654  naddcllem  8662  brecop  8808  brecop2  8809  eceqoveq  8820  xpdom2  9060  mapunen  9134  djuss  9906  djuunxp  9907  dfac5lem2  10108  iunfo  10523  ordpipq  10927  prsrlem1  11057  opelcn  11114  opelreal  11115  elreal2  11117  swrdnznd  14680  swrd00  14682  swrdcl  14683  swrd0  14696  pfx00  14712  pfx0  14713  fsumcom2  15825  fprodcom2  16038  phimullem  16838  imasvscafn  17591  homarcl2  18092  evlfcl  18278  clatl  18564  pzriprnglem4  21603  pzriprnglem9  21608  matplusgcell  22559  iscnp2  23365  txuni2  23691  txcls  23730  txcnpi  23734  txcnp  23746  txcnmpt  23750  txdis1cn  23761  txtube  23766  hausdiag  23771  txlm  23774  tx1stc  23776  txkgen  23778  txflf  24132  tmdcn2  24215  tgphaus  24243  qustgplem  24247  fmucndlem  24416  xmeterval  24558  metustexhalf  24682  blval2  24688  bcthlem1  25452  ovolfcl  25594  ovoliunlem1  25630  mbfimaopnlem  25783  limccnp2  26020  fsumvma  27343  lgsquadlem1  27510  lgsquadlem2  27511  norec2ov  28116  dmrab  32784  xppreima2  32937  aciunf1lem  32948  f1od2  33005  smatrcl  34131  smatlem  34132  qtophaus  34171  eulerpartlemgvv  34711  erdszelem10  35591  cvmlift2lem10  35703  cvmlift2lem12  35705  msubff  35921  elmpst  35927  mpstrcl  35932  elmpps  35964  dfso2  36146  fv1stcnv  36168  fv2ndcnv  36169  txpss3v  36267  dfrdg4  36342  bj-opelrelex  37676  bj-opelidres  37693  bj-elid6  37702  bj-eldiag2  37709  bj-inftyexpitaudisj  37737  curf  38137  curunc  38141  heiborlem3  38352  xrnss3v  38920  ecxrn2  38947  inxpxrn  38957  dibopelvalN  41807  dibopelval2  41809  dib1dim  41829  dihopcl  41917  dih1  41950  dih1dimatlem  41993  hdmap1val  42462  aks6d1c3  42780  pellex  43454  elnonrel  44203  mnringmulrcld  44844  fourierdlem42  46755  etransclem44  46884  ovn0lem  47171  ndmaovg  47810  aoprssdm  47828  ndmaovcl  47829  ndmaovrcl  47830  ndmaovcom  47831  ndmaovass  47832  ndmaovdistr  47833  sprsymrelfvlem  48128  sprsymrelfolem2  48131  prproropf1olem2  48142  opgpgvtx  48709  iinxp  49494  coxp  49496  joindm2  49631  meetdm2  49633  swapf2fval  49928  swapf1val  49930  fuco2el  49975