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

Theorem rspc 2991
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 2656 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2525 . . . 4  |-  F/_ x A
3 nfv 1626 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1822 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2449 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
7 rspc.2 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
86, 7imbi12d 312 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
92, 5, 8spcgf 2976 . . 3  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  -> 
( A  e.  B  ->  ps ) ) )
109pm2.43a 47 . 2  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  ->  ps ) )
111, 10syl5bi 209 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   F/wnf 1550    = wceq 1649    e. wcel 1717   A.wral 2651
This theorem is referenced by:  rspcv  2993  rspc2  3002  disjxiun  4152  pofun  4462  fmptcof  5843  fliftfuns  5977  qliftfuns  6929  xpf1o  7207  iunfi  7332  iundom2g  8350  lble  9894  rlimcld2  12301  sumeq2ii  12416  summolem3  12437  zsum  12441  fsum  12443  fsumf1o  12446  sumss2  12449  fsumcvg2  12450  fsumadd  12461  isummulc2  12475  fsum2dlem  12483  fsumcom2  12487  fsumshftm  12493  fsum0diag2  12495  fsummulc2  12496  fsum00  12506  fsumabs  12509  fsumrelem  12515  fsumrlim  12519  fsumo1  12520  o1fsum  12521  fsumiun  12529  isumshft  12548  pcmpt  13190  invfuc  14100  dprd2d2  15531  txcnp  17575  ptcnplem  17576  prdsdsf  18307  prdsxmet  18309  fsumcn  18773  ovolfiniun  19266  ovoliunnul  19272  volfiniun  19310  iunmbl  19316  limciun  19650  dvfsumle  19774  dvfsumabs  19776  dvfsumlem1  19779  dvfsumlem3  19781  dvfsumlem4  19782  dvfsumrlim  19784  dvfsumrlim2  19785  dvfsum2  19787  itgsubst  19802  fsumvma  20866  dchrisumlema  21051  dchrisumlem2  21053  dchrisumlem3  21054  chirred  23748  voliune  24381  volfiniune  24382  prodeq2ii  25020  prodmolem3  25040  zprod  25044  fprod  25048  fprodf1o  25053  prodss  25054  fprodser  25056  fprodmul  25065  fproddiv  25066  fprodm1s  25074  fprodp1s  25075  fprodabs  25078  fprodefsum  25079  tfisg  25230  ofmpteq  26469  mzpsubst  26498  rabdiophlem2  26555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-v 2903
  Copyright terms: Public domain W3C validator