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

Theorem rspc2ev 2905
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 2897 . . . 4  |-  ( ( B  e.  D  /\  ps )  ->  E. y  e.  D  ch )
32anim2i 552 . . 3  |-  ( ( A  e.  C  /\  ( B  e.  D  /\  ps ) )  -> 
( A  e.  C  /\  E. y  e.  D  ch ) )
433impb 1147 . 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 2577 . . 3  |-  ( x  =  A  ->  ( E. y  e.  D  ph  <->  E. y  e.  D  ch ) )
76rspcev 2897 . 2  |-  ( ( A  e.  C  /\  E. y  e.  D  ch )  ->  E. x  e.  C  E. y  e.  D  ph )
84, 7syl 15 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 176    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  rspc3ev  2907  opelxp  4735  rspceov  5909  erov  6771  2dom  6949  elfiun  7199  dffi3  7200  ixpiunwdom  7321  1re  8853  ello12r  12007  ello1d  12013  elo12r  12018  o1lo1  12027  addcn2  12083  mulcn2  12085  bezoutlem3  12735  bezout  12737  pythagtriplem18  12901  pczpre  12916  pcdiv  12921  4sqlem3  13013  4sqlem4  13015  4sqlem12  13019  vdwlem1  13044  vdwlem6  13049  vdwlem8  13051  vdwlem12  13055  vdwlem13  13056  0ram  13083  ramz2  13087  irredn0  15501  isnzr2  16031  hausnei2  17097  cnhaus  17098  dishaus  17126  ordthauslem  17127  txuni2  17276  xkoopn  17300  txopn  17313  txdis  17342  txdis1cn  17345  pthaus  17348  txhaus  17357  tx1stc  17360  xkohaus  17363  regr1lem  17446  divstgplem  17819  methaus  18082  met2ndci  18084  metnrmlem3  18381  elplyr  19599  aaliou2b  19737  aaliou3lem9  19746  2sqlem2  20619  2sqlem8  20627  2sqlem11  20630  2sqb  20633  pntibnd  20758  ofrn2  23222  lt2addrd  23264  xlt2addrd  23268  tpr2rico  23311  elsx  23540  isanmbfm  23576  br2base  23589  conpcon  23781  br8  24184  br4  24186  fprb  24200  axsegconlem1  24617  axsegcon  24627  axpaschlem  24640  axlowdimlem6  24647  axlowdim1  24659  axlowdim2  24660  axeuclidlem  24662  brsegle  24803  hilbert1.1  24849  rspc2edv  25066  repcpwti  25264  altretop  25703  nn0prpwlem  26341  cntotbnd  26623  smprngopr  26780  ralxpmap  26864  eldioph2lem1  26942  diophin  26955  fphpdo  27003  irrapxlem3  27012  irrapxlem4  27013  pellexlem6  27022  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell1234qrdich  27049  pell1qr1  27059  pellqrexplicit  27065  rmxycomplete  27105  dgraalem  27453  psgnunilem1  27519  rspceaov  28165  3cyclfrgrarn1  28435  4cycl2vnunb  28439  3dim2  30279  llni2  30323  lvoli3  30388  lvoli2  30392  islinei  30551  psubspi2N  30559  elpaddri  30613
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803
  Copyright terms: Public domain W3C validator