MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelxp Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 elxp2 5331 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 3393 . . . . . . 7 𝑥 ∈ V
3 vex 3393 . . . . . . 7 𝑦 ∈ V
42, 3opth2 5135 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2872 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2872 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 622 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 208 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 241 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 3223 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2805 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 4591 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2815 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 4592 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2815 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 3516 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1567 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 200 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 266 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator