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

Theorem rspccva 3573
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 3569 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 411 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873  df-ral 3114
This theorem is referenced by:  disjne  4365  n0snor2el  4727  seex  5486  preddowncl  6147  foelrn  6853  caofid0l  7421  caofid0r  7422  caofid1  7423  caofid2  7424  onnseq  7968  odi  8192  omsmolem  8267  fvixp  8453  unblem1  8758  ordiso2  8967  unwdomg  9036  ac5num  9451  acni2  9461  fodomacn  9471  iundom2g  9955  fpwwe2lem3  10048  eltsk2g  10166  tskpwss  10167  tskpw  10168  tsken  10169  prlem934  10448  dedekindle  10797  ltord1  11159  leord1  11160  eqord1  11161  ltord2  11162  leord2  11163  eqord2  11164  supmul1  11601  seqcaopr2  13406  bccl  13682  hashbc  13811  limsupbnd2  14835  2clim  14924  climsup  15021  caurcvg2  15029  caucvgb  15031  isummulc2  15112  telfsumo2  15153  fsumparts  15156  incexclem  15186  isumshft  15189  climcndslem1  15199  climcndslem2  15200  supcvg  15206  geomulcvg  15227  mertenslem2  15236  mertens  15237  bpolycl  15401  bpolydif  15404  rpnnen2lem10  15571  dvdsprime  16024  fuciso  17240  lubub  17724  lubl  17725  mgmlrid  17872  grprinvlem  17878  grpinvex  18108  issubg2  18289  issubg4  18293  nmzbi  18311  gagrpid  18419  cntzi  18454  psgnunilem2  18618  sylow1lem3  18720  pgpfi  18725  slwispgp  18731  sylow2alem1  18737  dprdfcl  19131  ablfac2  19207  abveq0  19593  issrngd  19628  phllmhm  20324  ipcl  20325  ipeq0  20330  isphld  20346  ocvi  20361  psrbagconf1o  20615  pf1ind  20982  cayhamlem3  21495  elcls3  21691  neindisj2  21731  perfi  21763  cnima  21873  1stcfb  22053  1stcelcls  22069  llyi  22082  nllyi  22083  locfinnei  22131  1stckgenlem  22161  ptbasin  22185  txcls  22212  ptcnp  22230  ufli  22522  tgpt0  22727  tsmsxplem2  22762  nrmmetd  23184  tngngp  23263  tngngp3  23265  reperflem  23426  lebnumlem3  23571  htpyi  23582  htpycc  23588  phtpyi  23592  cfili  23875  cmetcvg  23892  caubl  23915  caublcls  23916  bcthlem2  23932  bcthlem3  23933  bcthlem4  23934  ovolicc2lem1  24124  ovolicc2lem5  24128  ovolicc2  24129  voliunlem3  24159  volsuplem  24162  uniioombllem2  24190  mbfima  24237  ismbfd  24246  ismbf3d  24261  mbfmullem  24332  itg2monolem1  24357  itg2i1fseqle  24361  itg2i1fseq  24362  itg2i1fseq2  24363  itg2addlem  24365  bddmulibl  24445  bddiblnc  24448  c1liplem1  24602  dvfsumle  24627  dvfsumabs  24629  dvfsumrlimf  24631  dvfsumlem1  24632  dvfsumlem2  24633  dvfsumlem3  24634  dvfsumlem4  24635  dvfsumrlimge0  24636  dvfsum2  24640  ftc1lem6  24647  ulmcau  24993  ulmdvlem1  24998  ulmdvlem3  25000  mtestbdd  25003  itgulm  25006  radcnvlem1  25011  abelthlem5  25033  abelthlem7  25036  areambl  25547  2lgslem1a  25978  dchrisumlem2  26077  dchrvmasumiflem1  26088  pntpbnd1  26173  ostthlem1  26214  tglowdim1i  26298  brbtwn2  26702  ax5seglem1  26725  ax5seglem2  26726  ax5seglem9  26734  axcontlem4  26764  axcontlem12  26772  fusgreghash2wsp  28126  grpoidinvlem3  28292  grpoidinv  28294  grpoidinv2  28301  vcidOLD  28350  minvecolem5  28667  hcaucvg  28972  hlimconvi  28977  lnopeq0i  29793  cnlnadjlem5  29857  csmdsymi  30120  difelsiga  31500  eulerpartlemb  31734  ballotlemfc0  31858  ballotlemfcc  31859  ptpconn  32588  cvmsdisj  32625  cvmshmeo  32626  snmlflim  32687  elmrsubrn  32875  mvtinf  32910  sinccvg  33024  fnemeet1  33822  fnemeet2  33823  fnejoin1  33824  fnejoin2  33825  bj-seex  34360  poimirlem27  35077  poimirlem32  35082  mblfinlem1  35087  ovoliunnfl  35092  ex-ovoliunnfl  35093  voliunnfl  35094  volsupnfl  35095  mbfresfi  35096  itg2gt0cn  35105  ftc1cnnc  35122  ftc1anc  35131  upixp  35160  filbcmb  35171  sdclem1  35174  seqpo  35178  incsequz2  35180  mettrifi  35188  caushft  35192  sstotbnd2  35205  heibor1lem  35240  heiborlem3  35244  heiborlem10  35251  heibor  35252  rrndstprj2  35262  cmpidelt  35290  rngoid  35333  fsuppind  39443  limsuc2  39972  cvgdvgrat  41004  cncmpmax  41648  foelrnf  41800  mccllem  42226  mccl  42227  climinf  42235  climsuse  42237  islptre  42248  limcperiod  42257  addlimc  42277  0ellimcdiv  42278  cncficcgt0  42517  dvbdfbdioolem2  42558  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  dvnprodlem3  42577  stoweidlem7  42636  stoweidlem15  42644  stoweidlem21  42650  stoweidlem31  42660  stoweidlem35  42664  stoweidlem36  42665  stoweidlem50  42679  stoweidlem57  42686  stoweidlem59  42688  wallispilem3  42696  dirkercncflem2  42733  dirkercncflem4  42735  fourierdlem32  42768  fourierdlem33  42769  fourierdlem39  42775  fourierdlem62  42797  fourierdlem71  42806  fourierdlem89  42824  fourierdlem91  42826  fourierdlem93  42828  fourierdlem101  42836  fourierdlem103  42838  fourierdlem104  42839  etransclem24  42887  etransclem32  42895  smflimlem6  43396  smfpimcc  43426  smfsuplem2  43430  isomushgr  44331
  Copyright terms: Public domain W3C validator