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

Theorem rspccva 3619
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 3615 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 408 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  disjne  4400  n0snor2el  4756  seex  5511  preddowncl  6168  foelrn  6864  caofid0l  7426  caofid0r  7427  caofid1  7428  caofid2  7429  onnseq  7970  odi  8194  omsmolem  8269  fvixp  8454  unblem1  8758  ordiso2  8967  unwdomg  9036  ac5num  9450  acni2  9460  fodomacn  9470  iundom2g  9950  fpwwe2lem3  10043  eltsk2g  10161  tskpwss  10162  tskpw  10163  tsken  10164  prlem934  10443  dedekindle  10792  ltord1  11154  leord1  11155  eqord1  11156  ltord2  11157  leord2  11158  eqord2  11159  supmul1  11598  seqcaopr2  13394  bccl  13670  hashbc  13799  limsupbnd2  14828  2clim  14917  climsup  15014  caurcvg2  15022  caucvgb  15024  isummulc2  15105  telfsumo2  15146  fsumparts  15149  incexclem  15179  isumshft  15182  climcndslem1  15192  climcndslem2  15193  supcvg  15199  geomulcvg  15220  mertenslem2  15229  mertens  15230  bpolycl  15394  bpolydif  15397  rpnnen2lem10  15564  dvdsprime  16019  fuciso  17233  lubub  17717  lubl  17718  mgmlrid  17865  grprinvlem  17871  grpinvex  18051  issubg2  18232  issubg4  18236  nmzbi  18254  gagrpid  18362  cntzi  18397  psgnunilem2  18552  sylow1lem3  18654  pgpfi  18659  slwispgp  18665  sylow2alem1  18671  dprdfcl  19064  ablfac2  19140  abveq0  19526  issrngd  19561  psrbagconf1o  20082  pf1ind  20446  phllmhm  20704  ipcl  20705  ipeq0  20710  isphld  20726  ocvi  20741  cayhamlem3  21423  elcls3  21619  neindisj2  21659  perfi  21691  cnima  21801  1stcfb  21981  1stcelcls  21997  llyi  22010  nllyi  22011  locfinnei  22059  1stckgenlem  22089  ptbasin  22113  txcls  22140  ptcnp  22158  ufli  22450  tgpt0  22654  tsmsxplem2  22689  nrmmetd  23111  tngngp  23190  tngngp3  23192  reperflem  23353  lebnumlem3  23494  htpyi  23505  htpycc  23511  phtpyi  23515  cfili  23798  cmetcvg  23815  caubl  23838  caublcls  23839  bcthlem2  23855  bcthlem3  23856  bcthlem4  23857  ovolicc2lem1  24045  ovolicc2lem5  24049  ovolicc2  24050  voliunlem3  24080  volsuplem  24083  uniioombllem2  24111  mbfima  24158  ismbfd  24167  ismbf3d  24182  mbfmullem  24253  itg2monolem1  24278  itg2i1fseqle  24282  itg2i1fseq  24283  itg2i1fseq2  24284  itg2addlem  24286  bddmulibl  24366  c1liplem1  24520  dvfsumle  24545  dvfsumabs  24547  dvfsumrlimf  24549  dvfsumlem1  24550  dvfsumlem2  24551  dvfsumlem3  24552  dvfsumlem4  24553  dvfsumrlimge0  24554  dvfsum2  24558  ftc1lem6  24565  ulmcau  24910  ulmdvlem1  24915  ulmdvlem3  24917  mtestbdd  24920  itgulm  24923  radcnvlem1  24928  abelthlem5  24950  abelthlem7  24953  areambl  25463  2lgslem1a  25894  dchrisumlem2  25993  dchrvmasumiflem1  26004  pntpbnd1  26089  ostthlem1  26130  tglowdim1i  26214  brbtwn2  26618  ax5seglem1  26641  ax5seglem2  26642  ax5seglem9  26650  axcontlem4  26680  axcontlem12  26688  fusgreghash2wsp  28044  grpoidinvlem3  28210  grpoidinv  28212  grpoidinv2  28219  vcidOLD  28268  minvecolem5  28585  hcaucvg  28890  hlimconvi  28895  lnopeq0i  29711  cnlnadjlem5  29775  csmdsymi  30038  difelsiga  31291  eulerpartlemb  31525  ballotlemfc0  31649  ballotlemfcc  31650  ptpconn  32377  cvmsdisj  32414  cvmshmeo  32415  snmlflim  32476  elmrsubrn  32664  mvtinf  32699  sinccvg  32813  fnemeet1  33611  fnemeet2  33612  fnejoin1  33613  fnejoin2  33614  bj-seex  34138  poimirlem27  34800  poimirlem32  34805  mblfinlem1  34810  ovoliunnfl  34815  ex-ovoliunnfl  34816  voliunnfl  34817  volsupnfl  34818  mbfresfi  34819  itg2gt0cn  34828  bddiblnc  34843  ftc1cnnc  34847  ftc1anc  34856  upixp  34885  filbcmb  34896  sdclem1  34899  seqpo  34903  incsequz2  34905  mettrifi  34913  caushft  34917  sstotbnd2  34933  heibor1lem  34968  heiborlem3  34972  heiborlem10  34979  heibor  34980  rrndstprj2  34990  cmpidelt  35018  rngoid  35061  limsuc2  39519  cvgdvgrat  40522  cncmpmax  41166  foelrnf  41323  mccllem  41754  mccl  41755  climinf  41763  climsuse  41765  islptre  41776  limcperiod  41785  addlimc  41805  0ellimcdiv  41806  cncficcgt0  42047  dvbdfbdioolem2  42090  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnprodlem3  42109  stoweidlem7  42169  stoweidlem15  42177  stoweidlem21  42183  stoweidlem31  42193  stoweidlem35  42197  stoweidlem36  42198  stoweidlem50  42212  stoweidlem57  42219  stoweidlem59  42221  wallispilem3  42229  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem32  42301  fourierdlem33  42302  fourierdlem39  42308  fourierdlem62  42330  fourierdlem71  42339  fourierdlem89  42357  fourierdlem91  42359  fourierdlem93  42361  fourierdlem101  42369  fourierdlem103  42371  fourierdlem104  42372  etransclem24  42420  etransclem32  42428  smflimlem6  42929  smfpimcc  42959  smfsuplem2  42963  isomushgr  43868
  Copyright terms: Public domain W3C validator