Theorem opelxp 5695

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 5683	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3468	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3468	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5460	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2823	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2823	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 638	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3187	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2736	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4854	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2747	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4855	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2747	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3619	. . . 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 3061  ⟨cop 4612   × cxp 5657

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-opab 5187  df-xp 5665

This theorem is referenced by:  opelxpi  5696  opelxp1  5701  opelxp2  5702  otelxp  5703  otel3xp  5705  brxp  5708  opthprc  5723  elxp3  5725  opeliunxp  5726  opeliun2xp  5727  bropaex12  5751  optocl  5754  xpsspw  5793  inxp  5816  xpiindi  5820  opelres  5977  restidsing  6045  codir  6114  qfto  6115  xpnz  6153  difxp  6158  xpdifid  6162  dfco2  6239  relssdmrnOLD  6263  ressn  6279  opelf  6744  oprab4  7498  resoprab  7530  oprssdm  7593  nssdmovg  7594  ndmovg  7595  elmpocl  7653  fo1stres  8019  fo2ndres  8020  dfoprab4  8059  opiota  8063  bropopvvv  8094  bropfvvvvlem  8095  curry1  8108  xporderlem  8131  fnwelem  8135  frpoins3xpg  8144  xpord2lem  8146  xpord2pred  8149  xpord2indlem  8151  mpoxopxprcov0  8221  mpocurryd  8273  on2recsov  8685  naddcllem  8693  brecop  8829  brecop2  8830  eceqoveq  8841  xpdom2  9086  mapunen  9165  djuss  9939  djuunxp  9940  dfac5lem2  10143  iunfo  10558  ordpipq  10961  prsrlem1  11091  opelcn  11148  opelreal  11149  elreal2  11151  swrdnznd  14665  swrd00  14667  swrdcl  14668  swrd0  14681  pfx00  14697  pfx0  14698  fsumcom2  15795  fprodcom2  16005  phimullem  16803  imasvscafn  17556  homarcl2  18053  evlfcl  18239  clatl  18523  pzriprnglem4  21450  pzriprnglem9  21455  matplusgcell  22376  iscnp2  23182  txuni2  23508  txcls  23547  txcnpi  23551  txcnp  23563  txcnmpt  23567  txdis1cn  23578  txtube  23583  hausdiag  23588  txlm  23591  tx1stc  23593  txkgen  23595  txflf  23949  tmdcn2  24032  tgphaus  24060  qustgplem  24064  fmucndlem  24234  xmeterval  24376  metustexhalf  24500  blval2  24506  bcthlem1  25281  ovolfcl  25424  ovoliunlem1  25460  mbfimaopnlem  25613  limccnp2  25850  fsumvma  27181  lgsquadlem1  27348  lgsquadlem2  27349  norec2ov  27921  dmrab  32483  xppreima2  32634  aciunf1lem  32645  f1od2  32703  smatrcl  33832  smatlem  33833  qtophaus  33872  eulerpartlemgvv  34413  erdszelem10  35227  cvmlift2lem10  35339  cvmlift2lem12  35341  msubff  35557  elmpst  35563  mpstrcl  35568  elmpps  35600  dfso2  35777  fv1stcnv  35799  fv2ndcnv  35800  txpss3v  35901  dfrdg4  35974  bj-opelrelex  37167  bj-opelidres  37184  bj-elid6  37193  bj-eldiag2  37200  bj-inftyexpitaudisj  37228  curf  37627  curunc  37631  heiborlem3  37842  xrnss3v  38395  inxpxrn  38418  dibopelvalN  41167  dibopelval2  41169  dib1dim  41189  dihopcl  41277  dih1  41310  dih1dimatlem  41353  hdmap1val  41822  aks6d1c3  42141  pellex  42833  elnonrel  43584  mnringmulrcld  44227  fourierdlem42  46158  etransclem44  46287  ovn0lem  46574  ndmaovg  47193  aoprssdm  47211  ndmaovcl  47212  ndmaovrcl  47213  ndmaovcom  47214  ndmaovass  47215  ndmaovdistr  47216  sprsymrelfvlem  47484  sprsymrelfolem2  47487  prproropf1olem2  47498  opgpgvtx  48039  iinxp  48789  coxp  48791  joindm2  48922  meetdm2  48924  swapf2fval  49162  swapf1val  49164  fuco2el  49203