Theorem opelxp 5343

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 5331	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3393	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3393	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5135	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2872	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2872	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 622	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 208	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 241	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3223	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2805	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4591	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2815	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4592	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2815	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3516	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1567	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 200	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 266	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2158  ∃wrex 3096  ⟨cop 4373   × cxp 5306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-opab 4903  df-xp 5314

This theorem is referenced by:  brxp  5344  opelxpi  5345  opelxp1  5347  opelxp2  5348  otel3xp  5350  opthprc  5364  elxp3  5366  opeliunxp  5367  bropaex12  5391  optocl  5394  xpsspw  5431  xpiindi  5456  opelresg  5600  opelresOLD  5604  restidsing  5667  codir  5724  qfto  5725  xpnz  5761  difxp  5766  xpdifid  5770  ssrnres  5780  dfco2  5845  relssdmrn  5867  ressn  5882  opelf  6277  oprab4  6953  resoprab  6983  oprssdm  7042  nssdmovg  7043  ndmovg  7044  elmpt2cl  7103  resiexg  7329  fo1stres  7421  fo2ndres  7422  el2xptp0  7441  dfoprab4  7454  opiota  7458  bropopvvv  7486  bropfvvvvlem  7487  curry1  7500  curry2  7503  xporderlem  7519  fnwelem  7523  mpt2xopxprcov0  7575  mpt2curryd  7627  brecop  8072  brecop2  8073  brecop2OLD  8074  eceqoveq  8085  xpdom2  8291  mapunen  8365  djuss  9026  djuunxp  9027  dfac5lem2  9227  iunfo  9643  ordpipq  10046  prsrlem1  10175  opelcn  10232  opelreal  10233  elreal2  10235  swrd00  13637  swrdcl  13638  swrd0  13654  fsumcom2  14724  fprodcom2  14931  phimullem  15697  imasvscafn  16398  brcic  16658  homarcl2  16885  evlfcl  17063  clatl  17317  matplusgcell  20445  mdetrlin  20615  iscnp2  21253  txuni2  21578  txcls  21617  txcnpi  21621  txcnp  21633  txcnmpt  21637  txdis1cn  21648  txtube  21653  hausdiag  21658  txlm  21661  tx1stc  21663  txkgen  21665  txflf  22019  tmdcn2  22102  tgphaus  22129  qustgplem  22133  fmucndlem  22304  xmeterval  22446  metustexhalf  22570  blval2  22576  metuel2  22579  bcthlem1  23329  ovolfcl  23443  ovoliunlem1  23479  ovolshftlem1  23486  mbfimaopnlem  23632  limccnp2  23866  cxpcn3  24699  fsumvma  25148  lgsquadlem1  25315  lgsquadlem2  25316  ofresid  29768  xppreima2  29774  aciunf1lem  29786  f1od2  29823  smatrcl  30184  smatlem  30185  qtophaus  30225  eulerpartlemgvv  30760  erdszelem10  31502  cvmlift2lem10  31614  cvmlift2lem12  31616  msubff  31747  elmpst  31753  mpstrcl  31758  elmpps  31790  dfso2  31963  fv1stcnv  31997  fv2ndcnv  31998  txpss3v  32303  pprodss4v  32309  dfrdg4  32376  bj-elid3  33400  bj-eldiag2  33406  curf  33697  curunc  33701  heiborlem3  33920  opelresALTV  34346  xrnss3v  34444  inxpxrn  34463  dibopelvalN  36921  dibopelval2  36923  dib1dim  36943  dihopcl  37031  dih1  37064  dih1dimatlem  37107  hdmap1val  37576  pellex  37898  elnonrel  38388  fourierdlem42  40842  etransclem44  40971  ovn0lem  41258  ndmaovg  41770  aoprssdm  41788  ndmaovcl  41789  ndmaovrcl  41790  ndmaovcom  41791  ndmaovass  41792  ndmaovdistr  41793  pfx00  41956  pfx0  41957  sprsymrelfvlem  42305  sprsymrelfolem2  42308  opeliun2xp  42676