Theorem rspccv 3306

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

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	rspcv 3305	. 2 |- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	com12 32	1 |- ( A. x e. B ph -> ( A e. B -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  ssdifsn  4318  elinti  4485  trss  4761  fvn0ssdmfun  6350  dff3  6372  2fvcoidd  6552  ofrval  6907  limsuc  7049  limuni3  7052  frxp  7287  wfrdmcl  7423  smo11  7461  odi  7659  supub  8365  suplub  8366  elirrv  8504  dfom3  8544  noinfep  8557  oemapvali  8581  tcrank  8747  infxpenlem  8836  alephle  8911  dfac5lem5  8950  dfac2  8953  cofsmo  9091  coftr  9095  infpssrlem4  9128  isf34lem6  9202  axcc2lem  9258  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  axdc4lem  9277  ac5b  9300  zorn2lem2  9319  zorn2lem6  9323  pwcfsdom  9405  inar1  9597  grupw  9617  grupr  9619  gruurn  9620  grothpw  9648  grothpwex  9649  axgroth6  9650  grothomex  9651  nqereu  9751  supsrlem  9932  axpre-sup  9990  dedekind  10200  dedekindle  10201  supmullem1  10993  supmul  10995  peano5nni  11023  dfnn2  11033  peano5uzi  11466  zindd  11478  1arith  15631  ramcl  15733  clatleglb  17126  pslem  17206  cygabl  18292  eqcoe1ply1eq  19667  psgndiflemA  19947  mvmumamul1  20360  smadiadetlem0  20467  chpscmat  20647  basis2  20755  tg2  20769  clsndisj  20879  cnpimaex  21060  t1sncld  21130  regsep  21138  nrmsep3  21159  cmpsub  21203  2ndc1stc  21254  refssex  21314  ptfinfin  21322  txcnpi  21411  txcmplem1  21444  tx1stc  21453  filss  21657  ufilss  21709  fclsopni  21819  fclsrest  21828  alexsubb  21850  alexsubALTlem2  21852  alexsubALTlem4  21854  ghmcnp  21918  qustgplem  21924  mopni  22297  metrest  22329  metcnpi  22349  metcnpi2  22350  cfilucfil  22364  nmolb  22521  nmoleub2lem2  22916  ovoliunlem1  23270  ovolicc2lem3  23287  mblsplit  23300  fta1b  23929  plycj  24033  mtest  24158  lgamgulmlem1  24755  sqfpc  24863  ostth2lem2  25323  ostth3  25327  nbgrnself2  26259  vdiscusgr  26427  rusgrnumwrdl2  26482  ewlkinedg  26500  numclwwlk1  27231  l2p  27331  lpni  27332  nvz  27524  ubthlem2  27727  chcompl  28099  ocin  28155  hmopidmchi  29010  dmdmd  29159  dmdbr5  29167  mdsl1i  29180  sigaclci  30195  bnj23  30784  kur14lem9  31196  sconnpht  31211  cvmsdisj  31252  untelirr  31585  untsucf  31587  dfon2lem4  31691  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  frrlem5e  31788  sltval2  31809  fwddifnp1  32272  poimirlem18  33427  poimirlem21  33430  heibor1lem  33608  heiborlem4  33613  heiborlem6  33615  atlex  34603  psubspi  35033  elpcliN  35179  ldilval  35399  trlord  35857  tendotp  36049  hdmapval2  37124  pwelg  37865  gneispace0nelrn2  38439  gneispaceel2  38442  gneispacess2  38444  stoweid  40280  iccpartltu  41361  iccpartgtl  41362  iccpartleu  41364  iccpartgel  41365