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

Theorem rspc 2878
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1  |-  F/ x ps
rspc.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspc  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rspc
StepHypRef Expression
1 df-ral 2548 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2419 . . . 4  |-  F/_ x A
3 nfv 1605 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1769 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2343 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
7 rspc.2 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
86, 7imbi12d 311 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
92, 5, 8spcgf 2863 . . 3  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  -> 
( A  e.  B  ->  ps ) ) )
109pm2.43a 45 . 2  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  ->  ps ) )
111, 10syl5bi 208 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   F/wnf 1531    = wceq 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rspcv  2880  rspc2  2889  disjxiun  4020  pofun  4330  fmptcof  5692  fliftfuns  5813  qliftfuns  6745  xpf1o  7023  iunfi  7144  iundom2g  8162  lble  9706  rlimcld2  12052  sumeq2ii  12166  summolem3  12187  zsum  12191  fsum  12193  fsumf1o  12196  sumss2  12199  fsumcvg2  12200  fsumadd  12211  isummulc2  12225  fsum2dlem  12233  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsummulc2  12246  fsum00  12256  fsumabs  12259  fsumrelem  12265  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  isumshft  12298  pcmpt  12940  invfuc  13848  dprd2d2  15279  txcnp  17314  ptcnplem  17315  prdsdsf  17931  prdsxmet  17933  fsumcn  18374  ovolfiniun  18860  ovoliunnul  18866  volfiniun  18904  iunmbl  18910  limciun  19244  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsum2  19381  itgsubst  19396  fsumvma  20452  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  chirred  22975  tfisg  24204  prodeq3ii  25308  fprodadd  25352  fprodneg  25378  fprodsub  25379  ofmpteq  26797  mzpsubst  26826  rabdiophlem2  26883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator