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

Theorem opelxp 5670
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 5658 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 3448 . . . . . . 7 𝑥 ∈ V
3 vex 3448 . . . . . . 7 𝑦 ∈ V
42, 3opth2 5438 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2822 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2822 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 638 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 216 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 250 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 3193 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2733 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 4831 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2744 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 4832 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2744 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 3591 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1451 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 208 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 275 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wcel 2107  wrex 3070  cop 4593   × cxp 5632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5169  df-xp 5640
This theorem is referenced by:  opelxpi  5671  opelxp1  5675  opelxp2  5676  otelxp  5677  otel3xp  5679  brxp  5682  opthprc  5697  elxp3  5699  opeliunxp  5700  bropaex12  5724  optocl  5727  xpsspw  5766  xpiindi  5792  opelres  5944  restidsing  6007  codir  6075  qfto  6076  xpnz  6112  difxp  6117  xpdifid  6121  dfco2  6198  relssdmrnOLD  6222  ressn  6238  opelf  6704  oprab4  7444  resoprab  7475  oprssdm  7536  nssdmovg  7537  ndmovg  7538  elmpocl  7596  fo1stres  7948  fo2ndres  7949  dfoprab4  7988  opiota  7992  bropopvvv  8023  bropfvvvvlem  8024  curry1  8037  xporderlem  8060  fnwelem  8064  frpoins3xpg  8073  xpord2lem  8075  xpord2pred  8078  xpord2indlem  8080  mpoxopxprcov0  8149  mpocurryd  8201  on2recsov  8615  naddcllem  8623  brecop  8752  brecop2  8753  eceqoveq  8764  xpdom2  9014  mapunen  9093  djuss  9861  djuunxp  9862  dfac5lem2  10065  iunfo  10480  ordpipq  10883  prsrlem1  11013  opelcn  11070  opelreal  11071  elreal2  11073  swrdnznd  14536  swrd00  14538  swrdcl  14539  swrd0  14552  pfx00  14568  pfx0  14569  fsumcom2  15664  fprodcom2  15872  phimullem  16656  imasvscafn  17424  homarcl2  17926  evlfcl  18116  clatl  18402  matplusgcell  21798  iscnp2  22606  txuni2  22932  txcls  22971  txcnpi  22975  txcnp  22987  txcnmpt  22991  txdis1cn  23002  txtube  23007  hausdiag  23012  txlm  23015  tx1stc  23017  txkgen  23019  txflf  23373  tmdcn2  23456  tgphaus  23484  qustgplem  23488  fmucndlem  23659  xmeterval  23801  metustexhalf  23928  blval2  23934  bcthlem1  24704  ovolfcl  24846  ovoliunlem1  24882  mbfimaopnlem  25035  limccnp2  25272  fsumvma  26577  lgsquadlem1  26744  lgsquadlem2  26745  norec2ov  27291  dmrab  31468  xppreima2  31613  aciunf1lem  31624  f1od2  31685  smatrcl  32434  smatlem  32435  qtophaus  32474  eulerpartlemgvv  33033  erdszelem10  33851  cvmlift2lem10  33963  cvmlift2lem12  33965  msubff  34181  elmpst  34187  mpstrcl  34192  elmpps  34224  dfso2  34384  fv1stcnv  34407  fv2ndcnv  34408  txpss3v  34509  dfrdg4  34582  bj-opelrelex  35661  bj-opelidres  35678  bj-elid6  35687  bj-eldiag2  35694  bj-inftyexpitaudisj  35722  curf  36102  curunc  36106  heiborlem3  36318  xrnss3v  36880  inxpxrn  36903  dibopelvalN  39652  dibopelval2  39654  dib1dim  39674  dihopcl  39762  dih1  39795  dih1dimatlem  39838  hdmap1val  40307  pellex  41201  elnonrel  41945  mnringmulrcld  42596  fourierdlem42  44476  etransclem44  44605  ovn0lem  44892  ndmaovg  45502  aoprssdm  45520  ndmaovcl  45521  ndmaovrcl  45522  ndmaovcom  45523  ndmaovass  45524  ndmaovdistr  45525  sprsymrelfvlem  45768  sprsymrelfolem2  45771  prproropf1olem2  45782  opeliun2xp  46494  joindm2  47087  meetdm2  47089
  Copyright terms: Public domain W3C validator