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

Theorem rspc 3038
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 2702 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2571 . . . 4  |-  F/_ x A
3 nfv 1629 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1832 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2495 . . . . 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 3023 . . 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 1549   F/wnf 1553    = wceq 1652    e. wcel 1725   A.wral 2697
This theorem is referenced by:  rspcv  3040  rspc2  3049  disjxiun  4201  pofun  4511  fmptcof  5894  fliftfuns  6028  qliftfuns  6983  xpf1o  7261  iunfi  7386  iundom2g  8405  lble  9950  rlimcld2  12362  sumeq2ii  12477  summolem3  12498  zsum  12502  fsum  12504  fsumf1o  12507  sumss2  12510  fsumcvg2  12511  fsumadd  12522  isummulc2  12536  fsum2dlem  12544  fsumcom2  12548  fsumshftm  12554  fsum0diag2  12556  fsummulc2  12557  fsum00  12567  fsumabs  12570  fsumrelem  12576  fsumrlim  12580  fsumo1  12581  o1fsum  12582  fsumiun  12590  isumshft  12609  pcmpt  13251  invfuc  14161  dprd2d2  15592  txcnp  17642  ptcnplem  17643  prdsdsf  18387  prdsxmet  18389  fsumcn  18890  ovolfiniun  19387  ovoliunnul  19393  volfiniun  19431  iunmbl  19437  limciun  19771  dvfsumle  19895  dvfsumabs  19897  dvfsumlem1  19900  dvfsumlem3  19902  dvfsumlem4  19903  dvfsumrlim  19905  dvfsumrlim2  19906  dvfsum2  19908  itgsubst  19923  fsumvma  20987  dchrisumlema  21172  dchrisumlem2  21174  dchrisumlem3  21175  chirred  23888  voliune  24575  volfiniune  24576  prodeq2ii  25229  prodmolem3  25249  zprod  25253  fprod  25257  fprodf1o  25262  prodss  25263  fprodser  25265  fprodmul  25274  fproddiv  25275  fprodm1s  25283  fprodp1s  25284  fprodabs  25287  fprodefsum  25288  fprod2dlem  25294  fprodcom2  25298  tfisg  25464  ofmpteq  26730  mzpsubst  26759  rabdiophlem2  26816
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 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950
  Copyright terms: Public domain W3C validator