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

Theorem rspc2ev 3060
Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
Hypotheses
Ref Expression
rspc2v.1  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
rspc2v.2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
rspc2ev  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  E. x  e.  C  E. y  e.  D  ph )
Distinct variable groups:    x, y, A    y, B    x, C    x, D, y    ch, x    ps, y
Allowed substitution hints:    ph( x, y)    ps( x)    ch( y)    B( x)    C( y)

Proof of Theorem rspc2ev
StepHypRef Expression
1 rspc2v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
21rspcev 3052 . . . 4  |-  ( ( B  e.  D  /\  ps )  ->  E. y  e.  D  ch )
32anim2i 553 . . 3  |-  ( ( A  e.  C  /\  ( B  e.  D  /\  ps ) )  -> 
( A  e.  C  /\  E. y  e.  D  ch ) )
433impb 1149 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  ( A  e.  C  /\  E. y  e.  D  ch ) )
5 rspc2v.1 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
65rexbidv 2726 . . 3  |-  ( x  =  A  ->  ( E. y  e.  D  ph  <->  E. y  e.  D  ch ) )
76rspcev 3052 . 2  |-  ( ( A  e.  C  /\  E. y  e.  D  ch )  ->  E. x  e.  C  E. y  e.  D  ph )
84, 7syl 16 1  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  E. x  e.  C  E. y  e.  D  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725   E.wrex 2706
This theorem is referenced by:  rspc3ev  3062  opelxp  4908  rspceov  6116  erov  7001  2dom  7179  elfiun  7435  dffi3  7436  ixpiunwdom  7559  1re  9090  ello12r  12311  ello1d  12317  elo12r  12322  o1lo1  12331  addcn2  12387  mulcn2  12389  bezoutlem3  13040  bezout  13042  pythagtriplem18  13206  pczpre  13221  pcdiv  13226  4sqlem3  13318  4sqlem4  13320  4sqlem12  13324  vdwlem1  13349  vdwlem6  13354  vdwlem8  13356  vdwlem12  13360  vdwlem13  13361  0ram  13388  ramz2  13392  irredn0  15808  isnzr2  16334  hausnei2  17417  cnhaus  17418  dishaus  17446  ordthauslem  17447  txuni2  17597  xkoopn  17621  txopn  17634  txdis  17664  txdis1cn  17667  pthaus  17670  txhaus  17679  tx1stc  17682  xkohaus  17685  regr1lem  17771  divstgplem  18150  methaus  18550  met2ndci  18552  metnrmlem3  18891  elplyr  20120  aaliou2b  20258  aaliou3lem9  20267  2sqlem2  21148  2sqlem8  21156  2sqlem11  21159  2sqb  21162  pntibnd  21287  lt2addrd  24115  xlt2addrd  24124  xrnarchi  24254  pstmfval  24291  tpr2rico  24310  qqhval2  24366  elsx  24548  isanmbfm  24606  br2base  24619  dya2iocnrect  24631  conpcon  24922  br8  25379  br4  25381  fprb  25397  axsegconlem1  25856  axsegcon  25866  axpaschlem  25879  axlowdimlem6  25886  axlowdim1  25898  axlowdim2  25899  axeuclidlem  25901  brsegle  26042  hilbert1.1  26088  itg2addnclem3  26258  nn0prpwlem  26325  cntotbnd  26505  smprngopr  26662  ralxpmap  26742  eldioph2lem1  26818  diophin  26831  fphpdo  26878  irrapxlem3  26887  irrapxlem4  26888  pellexlem6  26897  pell1234qrreccl  26917  pell1234qrmulcl  26918  pell1234qrdich  26924  pell1qr1  26934  pellqrexplicit  26940  rmxycomplete  26980  dgraalem  27327  psgnunilem1  27393  rspceaov  28037  el2wlksotot  28349  3cyclfrgrarn1  28402  4cycl2vnunb  28407  3dim2  30265  llni2  30309  lvoli3  30374  lvoli2  30378  islinei  30537  psubspi2N  30545  elpaddri  30599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-v 2958
  Copyright terms: Public domain W3C validator