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

Theorem opelxp 5559
 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 5547 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 3447 . . . . . . 7 𝑥 ∈ V
3 vex 3447 . . . . . . 7 𝑦 ∈ V
42, 3opth2 5340 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2880 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2880 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 638 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 220 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 253 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 3254 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2801 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 4766 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2812 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 4768 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2812 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 3586 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1447 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 212 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 278 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∃wrex 3110  ⟨cop 4534   × cxp 5521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-opab 5096  df-xp 5529 This theorem is referenced by:  opelxpi  5560  opelxp1  5564  opelxp2  5565  otel3xp  5567  brxp  5569  opthprc  5584  elxp3  5586  opeliunxp  5587  bropaex12  5610  optocl  5613  xpsspw  5650  xpiindi  5674  opelres  5828  restidsing  5893  codir  5951  qfto  5952  xpnz  5987  difxp  5992  xpdifid  5996  dfco2  6069  relssdmrn  6092  ressn  6108  opelf  6517  oprab4  7223  resoprab  7253  oprssdm  7313  nssdmovg  7314  ndmovg  7315  elmpocl  7371  fo1stres  7701  fo2ndres  7702  dfoprab4  7739  opiota  7743  bropopvvv  7772  bropfvvvvlem  7773  curry1  7786  xporderlem  7808  fnwelem  7812  mpoxopxprcov0  7870  mpocurryd  7922  brecop  8377  brecop2  8378  eceqoveq  8389  xpdom2  8599  mapunen  8674  djuss  9337  djuunxp  9338  dfac5lem2  9539  iunfo  9954  ordpipq  10357  prsrlem1  10487  opelcn  10544  opelreal  10545  elreal2  10547  swrdnznd  13999  swrd00  14001  swrdcl  14002  swrd0  14015  pfx00  14031  pfx0  14032  fsumcom2  15125  fprodcom2  15334  phimullem  16110  imasvscafn  16806  homarcl2  17291  evlfcl  17468  clatl  17722  matplusgcell  21042  iscnp2  21848  txuni2  22174  txcls  22213  txcnpi  22217  txcnp  22229  txcnmpt  22233  txdis1cn  22244  txtube  22249  hausdiag  22254  txlm  22257  tx1stc  22259  txkgen  22261  txflf  22615  tmdcn2  22698  tgphaus  22726  qustgplem  22730  fmucndlem  22901  xmeterval  23043  metustexhalf  23167  blval2  23173  bcthlem1  23932  ovolfcl  24074  ovoliunlem1  24110  mbfimaopnlem  24263  limccnp2  24499  fsumvma  25801  lgsquadlem1  25968  lgsquadlem2  25969  dmrab  30271  xppreima2  30417  aciunf1lem  30429  f1od2  30487  smatrcl  31153  smatlem  31154  qtophaus  31193  eulerpartlemgvv  31748  erdszelem10  32561  cvmlift2lem10  32673  cvmlift2lem12  32675  msubff  32891  elmpst  32897  mpstrcl  32902  elmpps  32934  dfso2  33104  fv1stcnv  33134  fv2ndcnv  33135  txpss3v  33453  dfrdg4  33526  bj-opelrelex  34560  bj-opelidres  34577  bj-elid6  34586  bj-eldiag2  34593  bj-inftyexpitaudisj  34621  curf  35034  curunc  35038  heiborlem3  35250  xrnss3v  35783  inxpxrn  35802  dibopelvalN  38438  dibopelval2  38440  dib1dim  38460  dihopcl  38548  dih1  38581  dih1dimatlem  38624  hdmap1val  39093  pellex  39769  elnonrel  40278  mnringmulrcld  40929  fourierdlem42  42784  etransclem44  42913  ovn0lem  43197  ndmaovg  43733  aoprssdm  43751  ndmaovcl  43752  ndmaovrcl  43753  ndmaovcom  43754  ndmaovass  43755  ndmaovdistr  43756  sprsymrelfvlem  44000  sprsymrelfolem2  44003  prproropf1olem2  44014  opeliun2xp  44727
 Copyright terms: Public domain W3C validator