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

Theorem rspccv 3211
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspccv  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspccv
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3210 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 31 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115
This theorem is referenced by:  elinti  4291  dff3  6032  2fvcoidd  6186  ofrval  6532  limsuc  6662  limuni3  6665  frxp  6890  smo11  7032  odi  7225  supub  7915  suplub  7916  elirrv  8019  dfom3  8060  noinfep  8072  oemapvali  8099  tcrank  8298  infxpenlem  8387  alephle  8465  dfac5lem5  8504  dfac2  8507  cofsmo  8645  coftr  8649  infpssrlem4  8682  isf34lem6  8756  axcc2lem  8812  domtriomlem  8818  axdc2lem  8824  axdc3lem2  8827  axdc4lem  8831  ac5b  8854  zorn2lem2  8873  zorn2lem6  8877  pwcfsdom  8954  inar1  9149  grupw  9169  grupr  9171  gruurn  9172  grothpw  9200  grothpwex  9201  axgroth6  9202  grothomex  9203  nqereu  9303  supsrlem  9484  axpre-sup  9542  dedekind  9739  dedekindle  9740  supmullem1  10505  supmul  10507  peano5nni  10535  dfnn2  10545  peano5uzi  10945  zindd  10958  1arith  14300  ramcl  14402  clatleglb  15609  pslem  15689  cygabl  16684  eqcoe1ply1eq  18110  psgndiflemA  18404  smadiadetlem0  18930  chpscmat  19110  basis2  19219  tg2  19233  clsndisj  19342  cnpimaex  19523  t1sncld  19593  regsep  19601  nrmsep3  19622  cmpsub  19666  2ndc1stc  19718  txcnpi  19844  txcmplem1  19877  tx1stc  19886  filss  20089  ufilss  20141  fclsopni  20251  fclsrest  20260  alexsubb  20281  alexsubALTlem2  20283  alexsubALTlem4  20285  ghmcnp  20348  divstgplem  20354  mopni  20730  metrest  20762  metcnpi  20782  metcnpi2  20783  cfilucfilOLD  20807  cfilucfil  20808  nmolb  20959  nmoleub2lem2  21334  ovoliunlem1  21648  ovolicc2lem3  21665  mblsplit  21678  fta1b  22305  plycj  22408  mtest  22533  sqfpc  23139  ostth2lem2  23547  ostth3  23551  lpni  24857  nvz  25248  ubthlem2  25463  chcompl  25836  ocin  25890  hmopidmchi  26746  dmdmd  26895  dmdbr5  26903  mdsl1i  26916  sigaclci  27772  lgamgulmlem1  28211  kur14lem9  28298  sconpht  28314  cvmsdisj  28355  untelirr  28555  untsucf  28557  dfon2lem4  28795  dfon2lem6  28797  dfon2lem7  28798  dfon2lem8  28799  dfon2  28801  wfrlem9  28928  frrlem5e  28972  sltval2  28993  refssex  29753  ptfinfin  29770  heibor1lem  29908  heiborlem4  29913  heiborlem6  29915  stoweid  31363  bnj23  32851  atlex  34113  psubspi  34543  elpcliN  34689  ldilval  34909  trlord  35365  tendotp  35557  hdmapval2  36632
  Copyright terms: Public domain W3C validator