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

Theorem rspccva 3280
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 3277 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 444 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174
This theorem is referenced by:  disjne  3973  seex  4991  preddowncl  5610  foelrn  6271  grprinvlem  6748  caofid0l  6801  caofid0r  6802  caofid1  6803  caofid2  6804  onnseq  7306  odi  7524  omsmolem  7598  fvixp  7777  unblem1  8075  ordiso2  8281  unwdomg  8350  ac5num  8720  acni2  8730  fodomacn  8740  iundom2g  9219  fpwwe2lem3  9312  eltsk2g  9430  tskpwss  9431  tskpw  9432  tsken  9433  prlem934  9712  dedekindle  10053  ltord1  10406  leord1  10407  eqord1  10408  ltord2  10409  leord2  10410  eqord2  10411  supmul1  10842  seqcaopr2  12657  bccl  12929  hashbc  13049  limsupbnd2  14011  2clim  14100  climsup  14197  caurcvg2  14205  caucvgb  14207  isummulc2  14284  telfsumo2  14325  fsumparts  14328  incexclem  14356  isumshft  14359  climcndslem1  14369  climcndslem2  14370  supcvg  14376  geomulcvg  14395  mertenslem2  14405  mertens  14406  bpolycl  14571  bpolydif  14574  rpnnen2lem10  14740  dvdsprime  15187  iscatd2  16114  fuciso  16407  luble  16759  glble  16772  lubub  16891  lubl  16892  mgmlrid  17038  grpinvex  17204  issubg2  17381  issubg4  17385  nmzbi  17406  gagrpid  17499  cntzi  17534  psgnunilem2  17687  sylow1lem3  17787  pgpfi  17792  slwispgp  17798  sylow2alem1  17804  dprdfcl  18184  ablfac2  18260  abveq0  18598  issrngd  18633  psrbagconf1o  19144  pf1ind  19489  phllmhm  19744  ipcl  19745  ipeq0  19750  isphld  19766  ocvi  19780  cayhamlem3  20459  elcls3  20645  neindisj2  20685  perfi  20717  cnima  20827  1stcfb  21006  1stcelcls  21022  llyi  21035  nllyi  21036  locfinnei  21084  1stckgenlem  21114  ptbasin  21138  txcls  21165  ptcnp  21183  ufli  21476  tgpt0  21680  tsmsxplem2  21715  nrmmetd  22137  tngngp  22216  tngngp3  22218  reperflem  22377  lebnumlem3  22518  htpyi  22529  htpycc  22535  phtpyi  22539  cfili  22819  cmetcvg  22836  caubl  22859  caublcls  22860  bcthlem2  22875  bcthlem3  22876  bcthlem4  22877  ovolicc2lem1  23037  ovolicc2lem5  23041  ovolicc2  23042  voliunlem3  23072  volsuplem  23075  uniioombllem2  23102  mbfima  23150  ismbfd  23158  ismbf3d  23172  mbfmullem  23243  itg2monolem1  23268  itg2i1fseqle  23272  itg2i1fseq  23273  itg2i1fseq2  23274  itg2addlem  23276  bddmulibl  23356  c1liplem1  23508  dvfsumle  23533  dvfsumabs  23535  dvfsumrlimf  23537  dvfsumlem1  23538  dvfsumlem2  23539  dvfsumlem3  23540  dvfsumlem4  23541  dvfsumrlimge0  23542  dvfsum2  23546  ftc1lem6  23553  ulmcau  23898  ulmdvlem1  23903  ulmdvlem3  23905  mtestbdd  23908  itgulm  23911  radcnvlem1  23916  abelthlem5  23938  abelthlem7  23941  areambl  24430  2lgslem1a  24861  dchrisumlem2  24924  dchrvmasumiflem1  24935  pntpbnd1  25020  ostthlem1  25061  tglowdim1i  25141  brbtwn2  25531  ax5seglem1  25554  ax5seglem2  25555  ax5seglem9  25563  axcontlem4  25593  axcontlem12  25601  usgrcyclnl1  25962  eupaseg  26294  usgreghash2spot  26390  grpoidinvlem3  26538  grpoidinv  26540  grpoidinv2  26547  vcidOLD  26600  minvecolem5  26955  hcaucvg  27261  hlimconvi  27266  lnopeq0i  28084  cnlnadjlem5  28148  csmdsymi  28411  difelsiga  29357  eulerpartlemb  29591  ballotlemfc0  29715  ballotlemfcc  29716  ptpcon  30303  cvmsdisj  30340  cvmshmeo  30341  snmlflim  30402  elmrsubrn  30505  mvtinf  30540  sinccvg  30655  fnemeet1  31365  fnemeet2  31366  fnejoin1  31367  fnejoin2  31368  bj-seex  31935  poimirlem27  32430  poimirlem32  32435  mblfinlem1  32440  ovoliunnfl  32445  ex-ovoliunnfl  32446  voliunnfl  32447  volsupnfl  32448  mbfresfi  32450  itg2gt0cn  32459  bddiblnc  32474  ftc1cnnc  32478  ftc1anc  32487  upixp  32518  filbcmb  32529  sdclem1  32533  seqpo  32537  incsequz2  32539  mettrifi  32547  caushft  32551  sstotbnd2  32567  heibor1lem  32602  heiborlem3  32606  heiborlem10  32613  heibor  32614  rrndstprj2  32624  cmpidelt  32652  rngoid  32695  limsuc2  36453  cvgdvgrat  37358  cncmpmax  38038  foelrnf  38192  mccllem  38488  mccl  38489  climinf  38497  climsuse  38499  islptre  38510  limcperiod  38519  addlimc  38539  0ellimcdiv  38540  cncficcgt0  38598  fperdvper  38632  dvbdfbdioolem2  38643  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnprodlem3  38662  stoweidlem7  38724  stoweidlem15  38732  stoweidlem21  38738  stoweidlem31  38748  stoweidlem35  38752  stoweidlem36  38753  stoweidlem50  38767  stoweidlem57  38774  stoweidlem59  38776  wallispilem3  38784  dirkercncflem2  38821  dirkercncflem4  38823  fourierdlem32  38856  fourierdlem33  38857  fourierdlem39  38863  fourierdlem62  38885  fourierdlem71  38894  fourierdlem89  38912  fourierdlem91  38914  fourierdlem93  38916  fourierdlem101  38924  fourierdlem103  38926  fourierdlem104  38927  etransclem24  38975  etransclem32  38983  smflimlem6  39486  0vtxrusgr  40799  fusgreghash2wsp  41524
  Copyright terms: Public domain W3C validator