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

Theorem opelxp 5116
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 5102 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 3193 . . . . . . 7 𝑥 ∈ V
3 vex 3193 . . . . . . 7 𝑦 ∈ V
42, 3opth2 4919 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2686 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2686 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 916 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 207 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 240 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 3031 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2621 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 4377 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2631 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 4378 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2631 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 3313 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1410 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 199 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 264 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wcel 1987  wrex 2909  cop 4161   × cxp 5082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-opab 4684  df-xp 5090
This theorem is referenced by:  brxp  5117  opelxpi  5118  opelxp1  5120  opelxp2  5121  otel3xp  5123  opthprc  5137  elxp3  5140  opeliunxp  5141  bropaex12  5163  optocl  5166  xpsspw  5204  xpiindi  5227  opelres  5371  restidsing  5427  restidsingOLD  5428  codir  5485  qfto  5486  xpnz  5522  difxp  5527  xpdifid  5531  ssrnres  5541  dfco2  5603  relssdmrn  5625  ressn  5640  elsnxpOLD  5647  opelf  6032  oprab4  6691  resoprab  6721  oprssdm  6780  nssdmovg  6781  ndmovg  6782  elmpt2cl  6841  resiexg  7064  fo1stres  7152  fo2ndres  7153  el2xptp0  7172  dfoprab4  7185  opiota  7189  bropopvvv  7215  bropfvvvvlem  7216  curry1  7229  curry2  7232  xporderlem  7248  fnwelem  7252  mpt2xopxprcov0  7303  mpt2curryd  7355  brecop  7800  brecop2  7801  eceqoveq  7813  xpdom2  8015  mapunen  8089  dfac5lem2  8907  iunfo  9321  ordpipq  9724  prsrlem1  9853  opelcn  9910  opelreal  9911  elreal2  9913  swrd00  13372  swrdcl  13373  swrd0  13388  fsumcom2  14452  fsumcom2OLD  14453  fprodcom2  14658  fprodcom2OLD  14659  phimullem  15427  imasvscafn  16137  brcic  16398  homarcl2  16625  evlfcl  16802  clatl  17056  matplusgcell  20179  mdetrlin  20348  iscnp2  20983  txuni2  21308  txcls  21347  txcnpi  21351  txcnp  21363  txcnmpt  21367  txdis1cn  21378  txtube  21383  hausdiag  21388  txlm  21391  tx1stc  21393  txkgen  21395  txflf  21750  tmdcn2  21833  tgphaus  21860  qustgplem  21864  fmucndlem  22035  xmeterval  22177  metustexhalf  22301  blval2  22307  metuel2  22310  bcthlem1  23061  ovolfcl  23175  ovoliunlem1  23210  ovolshftlem1  23217  mbfimaopnlem  23362  limccnp2  23596  cxpcn3  24423  fsumvma  24872  lgsquadlem1  25039  lgsquadlem2  25040  ofresid  29327  xppreima2  29333  aciunf1lem  29345  f1od2  29383  smatrcl  29686  smatlem  29687  qtophaus  29727  eulerpartlemgvv  30261  erdszelem10  30943  cvmlift2lem10  31055  cvmlift2lem12  31057  msubff  31188  elmpst  31194  mpstrcl  31199  elmpps  31231  dfso2  31405  fv1stcnv  31435  fv2ndcnv  31436  txpss3v  31680  pprodss4v  31686  dfrdg4  31753  bj-elid3  32759  bj-eldiag2  32764  curf  33058  curunc  33062  heiborlem3  33283  dibopelvalN  35951  dibopelval2  35953  dib1dim  35973  dihopcl  36061  dih1  36094  dih1dimatlem  36137  hdmap1val  36607  pellex  36918  elnonrel  37411  fourierdlem42  39703  etransclem44  39832  ovn0lem  40116  ndmaovg  40598  aoprssdm  40616  ndmaovcl  40617  ndmaovrcl  40618  ndmaovcom  40619  ndmaovass  40620  ndmaovdistr  40621  pfx00  40713  pfx0  40714  sprsymrelfvlem  41058  sprsymrelfolem2  41061  opeliun2xp  41429
  Copyright terms: Public domain W3C validator