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

Theorem rspc2ev 3593
Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
Hypotheses
Ref Expression
rspc2v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc2v.2 (𝑦 = 𝐵 → (𝜒𝜓))
Assertion
Ref Expression
rspc2ev ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev
StepHypRef Expression
1 rspc2v.2 . . . . 5 (𝑦 = 𝐵 → (𝜒𝜓))
21rspcev 3582 . . . 4 ((𝐵𝐷𝜓) → ∃𝑦𝐷 𝜒)
32anim2i 618 . . 3 ((𝐴𝐶 ∧ (𝐵𝐷𝜓)) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
433impb 1116 . 2 ((𝐴𝐶𝐵𝐷𝜓) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
5 rspc2v.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜒))
65rexbidv 3176 . . 3 (𝑥 = 𝐴 → (∃𝑦𝐷 𝜑 ↔ ∃𝑦𝐷 𝜒))
76rspcev 3582 . 2 ((𝐴𝐶 ∧ ∃𝑦𝐷 𝜒) → ∃𝑥𝐶𝑦𝐷 𝜑)
84, 7syl 17 1 ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wrex 3074
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075
This theorem is referenced by:  rspc3ev  3595  opelxp  5670  fprb  7144  f1prex  7231  nf1const  7251  rspceov  7405  erov  8754  ralxpmap  8835  2dom  8975  elfiun  9367  dffi3  9368  ixpiunwdom  9527  1re  11156  hashdmpropge2  14383  wrdl2exs2  14836  ello12r  15400  ello1d  15406  elo12r  15411  o1lo1  15420  addcn2  15477  mulcn2  15479  bezoutlem3  16423  bezout  16425  pythagtriplem18  16705  pczpre  16720  pcdiv  16725  4sqlem3  16823  4sqlem4  16825  4sqlem12  16829  vdwlem1  16854  vdwlem6  16859  vdwlem8  16861  vdwlem12  16865  vdwlem13  16866  0ram  16893  ramz2  16897  cat1lem  17983  sgrp2rid2ex  18738  pmtr3ncom  19258  psgnunilem1  19276  irredn0  20133  isnzr2  20736  hausnei2  22707  cnhaus  22708  dishaus  22736  ordthauslem  22737  txuni2  22919  xkoopn  22943  txopn  22956  txdis  22986  txdis1cn  22989  pthaus  22992  txhaus  23001  tx1stc  23004  xkohaus  23007  regr1lem  23093  qustgplem  23475  methaus  23879  met2ndci  23881  metnrmlem3  24227  elplyr  25565  aaliou2b  25704  aaliou3lem9  25713  2irrexpq  26088  2irrexpqALT  26153  2sqlem2  26769  2sqlem8  26777  2sqlem11  26780  2sqb  26783  2sqnn0  26789  2sqnn  26790  pntibnd  26944  madecut  27215  legov  27530  iscgrad  27756  f1otrge  27817  axsegconlem1  27869  axsegcon  27879  axpaschlem  27892  axlowdimlem6  27899  axlowdim1  27911  axlowdim2  27912  axeuclidlem  27914  umgrvad2edg  28164  wwlksnwwlksnon  28863  upgr4cycl4dv4e  29132  3cyclfrgrrn1  29232  4cycl2vnunb  29237  br8d  31532  lt2addrd  31659  xlt2addrd  31666  xrnarchi  32023  txomap  32418  tpr2rico  32496  qqhval2  32566  elsx  32796  br2base  32872  dya2iocnrect  32884  connpconn  33832  satfv1fvfmla1  34020  br8  34332  br4  34334  brsegle  34696  hilbert1.1  34742  nn0prpwlem  34797  knoppndvlem21  34998  poimirlem1  36082  itg2addnclem3  36134  cntotbnd  36258  smprngopr  36514  3dim2  37934  llni2  37978  lvoli3  38043  lvoli2  38047  islinei  38206  psubspi2N  38214  elpaddri  38268  2rspcedvdw  40635  eldioph2lem1  41086  diophin  41098  fphpdo  41143  irrapxlem3  41150  irrapxlem4  41151  pellexlem6  41160  pell1234qrreccl  41180  pell1234qrmulcl  41181  pell1234qrdich  41187  pell1qr1  41197  pellqrexplicit  41203  rmxycomplete  41244  dgraalem  41475  clsk3nimkb  42319  fourierdlem64  44418  rspceaov  45436  ichnreuop  45671  prelspr  45685  reuopreuprim  45725  6gbe  45970  7gbow  45971  8gbe  45972  9gbo  45973  11gbo  45974  modn0mul  46613  elbigo2r  46646  rrx2xpref1o  46811  inlinecirc02plem  46879  sepfsepc  46967  iscnrm3lem7  46979
  Copyright terms: Public domain W3C validator