MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspccva Structured version   Visualization version   GIF version

Theorem rspccva 3497
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspccva ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccva
StepHypRef Expression
1 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
21rspcv 3494 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 396 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2155  wral 3092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-v 3389
This theorem is referenced by:  disjne  4213  n0snor2el  4546  seex  5268  preddowncl  5914  foelrn  6594  grprinvlem  7096  caofid0l  7149  caofid0r  7150  caofid1  7151  caofid2  7152  onnseq  7671  odi  7890  omsmolem  7964  fvixp  8144  unblem1  8445  ordiso2  8653  unwdomg  8722  ac5num  9136  acni2  9146  fodomacn  9156  iundom2g  9641  fpwwe2lem3  9734  eltsk2g  9852  tskpwss  9853  tskpw  9854  tsken  9855  prlem934  10134  dedekindle  10480  ltord1  10833  leord1  10834  eqord1  10835  ltord2  10836  leord2  10837  eqord2  10838  supmul1  11271  seqcaopr2  13054  bccl  13323  hashbc  13448  limsupbnd2  14431  2clim  14520  climsup  14617  caurcvg2  14625  caucvgb  14627  isummulc2  14710  telfsumo2  14751  fsumparts  14754  incexclem  14784  isumshft  14787  climcndslem1  14797  climcndslem2  14798  supcvg  14804  geomulcvg  14823  mertenslem2  14832  mertens  14833  bpolycl  14997  bpolydif  15000  rpnnen2lem10  15166  dvdsprime  15612  fuciso  16833  lubub  17318  lubl  17319  mgmlrid  17465  grpinvex  17631  issubg2  17805  issubg4  17809  nmzbi  17830  gagrpid  17922  cntzi  17957  psgnunilem2  18110  sylow1lem3  18210  pgpfi  18215  slwispgp  18221  sylow2alem1  18227  dprdfcl  18608  ablfac2  18684  abveq0  19024  issrngd  19059  psrbagconf1o  19577  pf1ind  19921  phllmhm  20181  ipcl  20182  ipeq0  20187  isphld  20203  ocvi  20217  cayhamlem3  20899  elcls3  21095  neindisj2  21135  perfi  21167  cnima  21277  1stcfb  21456  1stcelcls  21472  llyi  21485  nllyi  21486  locfinnei  21534  1stckgenlem  21564  ptbasin  21588  txcls  21615  ptcnp  21633  ufli  21925  tgpt0  22129  tsmsxplem2  22164  nrmmetd  22586  tngngp  22665  tngngp3  22667  reperflem  22828  lebnumlem3  22969  htpyi  22980  htpycc  22986  phtpyi  22990  cfili  23272  cmetcvg  23289  caubl  23312  caublcls  23313  bcthlem2  23328  bcthlem3  23329  bcthlem4  23330  ovolicc2lem1  23492  ovolicc2lem5  23496  ovolicc2  23497  voliunlem3  23527  volsuplem  23530  uniioombllem2  23558  mbfima  23605  ismbfd  23614  ismbf3d  23629  mbfmullem  23700  itg2monolem1  23725  itg2i1fseqle  23729  itg2i1fseq  23730  itg2i1fseq2  23731  itg2addlem  23733  bddmulibl  23813  c1liplem1  23967  dvfsumle  23992  dvfsumabs  23994  dvfsumrlimf  23996  dvfsumlem1  23997  dvfsumlem2  23998  dvfsumlem3  23999  dvfsumlem4  24000  dvfsumrlimge0  24001  dvfsum2  24005  ftc1lem6  24012  ulmcau  24357  ulmdvlem1  24362  ulmdvlem3  24364  mtestbdd  24367  itgulm  24370  radcnvlem1  24375  abelthlem5  24397  abelthlem7  24400  areambl  24893  2lgslem1a  25324  dchrisumlem2  25387  dchrvmasumiflem1  25398  pntpbnd1  25483  ostthlem1  25524  tglowdim1i  25604  brbtwn2  25993  ax5seglem1  26016  ax5seglem2  26017  ax5seglem9  26025  axcontlem4  26055  axcontlem12  26063  0vtxrusgr  26695  fusgreghash2wsp  27507  grpoidinvlem3  27683  grpoidinv  27685  grpoidinv2  27692  vcidOLD  27741  minvecolem5  28059  hcaucvg  28365  hlimconvi  28370  lnopeq0i  29188  cnlnadjlem5  29252  csmdsymi  29515  difelsiga  30515  eulerpartlemb  30749  ballotlemfc0  30873  ballotlemfcc  30874  ptpconn  31532  cvmsdisj  31569  cvmshmeo  31570  snmlflim  31631  elmrsubrn  31734  mvtinf  31769  sinccvg  31883  fnemeet1  32676  fnemeet2  32677  fnejoin1  32678  fnejoin2  32679  bj-seex  33223  poimirlem27  33743  poimirlem32  33748  mblfinlem1  33753  ovoliunnfl  33758  ex-ovoliunnfl  33759  voliunnfl  33760  volsupnfl  33761  mbfresfi  33762  itg2gt0cn  33771  bddiblnc  33786  ftc1cnnc  33790  ftc1anc  33799  upixp  33830  filbcmb  33841  sdclem1  33844  seqpo  33848  incsequz2  33850  mettrifi  33858  caushft  33862  sstotbnd2  33878  heibor1lem  33913  heiborlem3  33917  heiborlem10  33924  heibor  33925  rrndstprj2  33935  cmpidelt  33963  rngoid  34006  limsuc2  38106  cvgdvgrat  39006  cncmpmax  39679  foelrnf  39856  mccllem  40303  mccl  40304  climinf  40312  climsuse  40314  islptre  40325  limcperiod  40334  addlimc  40354  0ellimcdiv  40355  cncficcgt0  40575  dvbdfbdioolem2  40618  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  dvnprodlem3  40637  stoweidlem7  40697  stoweidlem15  40705  stoweidlem21  40711  stoweidlem31  40721  stoweidlem35  40725  stoweidlem36  40726  stoweidlem50  40740  stoweidlem57  40747  stoweidlem59  40749  wallispilem3  40757  dirkercncflem2  40794  dirkercncflem4  40796  fourierdlem32  40829  fourierdlem33  40830  fourierdlem39  40836  fourierdlem62  40858  fourierdlem71  40867  fourierdlem89  40885  fourierdlem91  40887  fourierdlem93  40889  fourierdlem101  40897  fourierdlem103  40899  fourierdlem104  40900  etransclem24  40948  etransclem32  40956  smflimlem6  41460  smfpimcc  41490  smfsuplem2  41494
  Copyright terms: Public domain W3C validator