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

Theorem rspccv 3075
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 3074 . 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 1369    e. wcel 1756   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-v 2979
This theorem is referenced by:  elinti  4142  dff3  5861  ofrval  6335  limsuc  6465  limuni3  6468  frxp  6687  smo11  6830  odi  7023  supub  7714  suplub  7715  elirrv  7817  dfom3  7858  noinfep  7870  oemapvali  7897  tcrank  8096  infxpenlem  8185  alephle  8263  dfac5lem5  8302  dfac2  8305  cofsmo  8443  coftr  8447  infpssrlem4  8480  isf34lem6  8554  axcc2lem  8610  domtriomlem  8616  axdc2lem  8622  axdc3lem2  8625  axdc4lem  8629  ac5b  8652  zorn2lem2  8671  zorn2lem6  8675  pwcfsdom  8752  inar1  8947  grupw  8967  grupr  8969  gruurn  8970  grothpw  8998  grothpwex  8999  axgroth6  9000  grothomex  9001  nqereu  9103  supsrlem  9283  axpre-sup  9341  dedekind  9538  dedekindle  9539  supmullem1  10301  supmul  10303  peano5nni  10330  dfnn2  10340  peano5uzi  10735  zindd  10748  1arith  13993  ramcl  14095  clatleglb  15301  pslem  15381  cygabl  16372  psgndiflemA  18036  smadiadetlem0  18472  basis2  18561  tg2  18575  clsndisj  18684  cnpimaex  18865  t1sncld  18935  regsep  18943  nrmsep3  18964  cmpsub  19008  2ndc1stc  19060  txcnpi  19186  txcmplem1  19219  tx1stc  19228  filss  19431  ufilss  19483  fclsopni  19593  fclsrest  19602  alexsubb  19623  alexsubALTlem2  19625  alexsubALTlem4  19627  ghmcnp  19690  divstgplem  19696  mopni  20072  metrest  20104  metcnpi  20124  metcnpi2  20125  cfilucfilOLD  20149  cfilucfil  20150  nmolb  20301  nmoleub2lem2  20676  ovoliunlem1  20990  ovolicc2lem3  21007  mblsplit  21020  fta1b  21646  plycj  21749  mtest  21874  sqfpc  22480  ostth2lem2  22888  ostth3  22892  lpni  23671  nvz  24062  ubthlem2  24277  chcompl  24650  ocin  24704  hmopidmchi  25560  dmdmd  25709  dmdbr5  25717  mdsl1i  25730  sigaclci  26580  lgamgulmlem1  27020  kur14lem9  27107  sconpht  27123  cvmsdisj  27164  untelirr  27364  untsucf  27366  dfon2lem4  27604  dfon2lem6  27606  dfon2lem7  27607  dfon2lem8  27608  dfon2  27610  wfrlem9  27737  frrlem5e  27781  sltval2  27802  refssex  28558  ptfinfin  28575  heibor1lem  28713  heiborlem4  28718  heiborlem6  28720  stoweid  29863  eqcoe1ply1eq  30840  bnj23  31712  atlex  32966  psubspi  33396  elpcliN  33542  ldilval  33762  trlord  34218  tendotp  34410  hdmapval2  35485
  Copyright terms: Public domain W3C validator