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

Theorem rspccva 3621
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 3617 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 408 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3138
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143
This theorem is referenced by:  disjne  4402  n0snor2el  4758  seex  5512  preddowncl  6169  foelrn  6865  caofid0l  7426  caofid0r  7427  caofid1  7428  caofid2  7429  onnseq  7972  odi  8195  omsmolem  8270  fvixp  8455  unblem1  8759  ordiso2  8968  unwdomg  9037  ac5num  9451  acni2  9461  fodomacn  9471  iundom2g  9951  fpwwe2lem3  10044  eltsk2g  10162  tskpwss  10163  tskpw  10164  tsken  10165  prlem934  10444  dedekindle  10793  ltord1  11155  leord1  11156  eqord1  11157  ltord2  11158  leord2  11159  eqord2  11160  supmul1  11599  seqcaopr2  13396  bccl  13672  hashbc  13801  limsupbnd2  14830  2clim  14919  climsup  15016  caurcvg2  15024  caucvgb  15026  isummulc2  15107  telfsumo2  15148  fsumparts  15151  incexclem  15181  isumshft  15184  climcndslem1  15194  climcndslem2  15195  supcvg  15201  geomulcvg  15222  mertenslem2  15231  mertens  15232  bpolycl  15396  bpolydif  15399  rpnnen2lem10  15566  dvdsprime  16021  fuciso  17235  lubub  17719  lubl  17720  mgmlrid  17867  grprinvlem  17873  grpinvex  18053  issubg2  18234  issubg4  18238  nmzbi  18256  gagrpid  18364  cntzi  18399  psgnunilem2  18554  sylow1lem3  18656  pgpfi  18661  slwispgp  18667  sylow2alem1  18673  dprdfcl  19066  ablfac2  19142  abveq0  19528  issrngd  19563  psrbagconf1o  20084  pf1ind  20448  phllmhm  20706  ipcl  20707  ipeq0  20712  isphld  20728  ocvi  20743  cayhamlem3  21425  elcls3  21621  neindisj2  21661  perfi  21693  cnima  21803  1stcfb  21983  1stcelcls  21999  llyi  22012  nllyi  22013  locfinnei  22061  1stckgenlem  22091  ptbasin  22115  txcls  22142  ptcnp  22160  ufli  22452  tgpt0  22656  tsmsxplem2  22691  nrmmetd  23113  tngngp  23192  tngngp3  23194  reperflem  23355  lebnumlem3  23496  htpyi  23507  htpycc  23513  phtpyi  23517  cfili  23800  cmetcvg  23817  caubl  23840  caublcls  23841  bcthlem2  23857  bcthlem3  23858  bcthlem4  23859  ovolicc2lem1  24047  ovolicc2lem5  24051  ovolicc2  24052  voliunlem3  24082  volsuplem  24085  uniioombllem2  24113  mbfima  24160  ismbfd  24169  ismbf3d  24184  mbfmullem  24255  itg2monolem1  24280  itg2i1fseqle  24284  itg2i1fseq  24285  itg2i1fseq2  24286  itg2addlem  24288  bddmulibl  24368  c1liplem1  24522  dvfsumle  24547  dvfsumabs  24549  dvfsumrlimf  24551  dvfsumlem1  24552  dvfsumlem2  24553  dvfsumlem3  24554  dvfsumlem4  24555  dvfsumrlimge0  24556  dvfsum2  24560  ftc1lem6  24567  ulmcau  24912  ulmdvlem1  24917  ulmdvlem3  24919  mtestbdd  24922  itgulm  24925  radcnvlem1  24930  abelthlem5  24952  abelthlem7  24955  areambl  25464  2lgslem1a  25895  dchrisumlem2  25994  dchrvmasumiflem1  26005  pntpbnd1  26090  ostthlem1  26131  tglowdim1i  26215  brbtwn2  26619  ax5seglem1  26642  ax5seglem2  26643  ax5seglem9  26651  axcontlem4  26681  axcontlem12  26689  fusgreghash2wsp  28045  grpoidinvlem3  28211  grpoidinv  28213  grpoidinv2  28220  vcidOLD  28269  minvecolem5  28586  hcaucvg  28891  hlimconvi  28896  lnopeq0i  29712  cnlnadjlem5  29776  csmdsymi  30039  difelsiga  31292  eulerpartlemb  31526  ballotlemfc0  31650  ballotlemfcc  31651  ptpconn  32378  cvmsdisj  32415  cvmshmeo  32416  snmlflim  32477  elmrsubrn  32665  mvtinf  32700  sinccvg  32814  fnemeet1  33612  fnemeet2  33613  fnejoin1  33614  fnejoin2  33615  bj-seex  34139  poimirlem27  34801  poimirlem32  34806  mblfinlem1  34811  ovoliunnfl  34816  ex-ovoliunnfl  34817  voliunnfl  34818  volsupnfl  34819  mbfresfi  34820  itg2gt0cn  34829  bddiblnc  34844  ftc1cnnc  34848  ftc1anc  34857  upixp  34887  filbcmb  34898  sdclem1  34901  seqpo  34905  incsequz2  34907  mettrifi  34915  caushft  34919  sstotbnd2  34935  heibor1lem  34970  heiborlem3  34974  heiborlem10  34981  heibor  34982  rrndstprj2  34992  cmpidelt  35020  rngoid  35063  limsuc2  39521  cvgdvgrat  40525  cncmpmax  41169  foelrnf  41327  mccllem  41758  mccl  41759  climinf  41767  climsuse  41769  islptre  41780  limcperiod  41789  addlimc  41809  0ellimcdiv  41810  cncficcgt0  42051  dvbdfbdioolem2  42094  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnprodlem3  42113  stoweidlem7  42173  stoweidlem15  42181  stoweidlem21  42187  stoweidlem31  42197  stoweidlem35  42201  stoweidlem36  42202  stoweidlem50  42216  stoweidlem57  42223  stoweidlem59  42225  wallispilem3  42233  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem32  42305  fourierdlem33  42306  fourierdlem39  42312  fourierdlem62  42334  fourierdlem71  42343  fourierdlem89  42361  fourierdlem91  42363  fourierdlem93  42365  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  etransclem24  42424  etransclem32  42432  smflimlem6  42933  smfpimcc  42963  smfsuplem2  42967  isomushgr  43838
  Copyright terms: Public domain W3C validator