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

Theorem rspccva 3436
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 3433 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 445 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wcel 2127  wral 3038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-v 3330
This theorem is referenced by:  disjne  4153  n0snor2el  4497  seex  5217  preddowncl  5856  foelrn  6529  grprinvlem  7025  caofid0l  7078  caofid0r  7079  caofid1  7080  caofid2  7081  onnseq  7598  odi  7816  omsmolem  7890  fvixp  8067  unblem1  8365  ordiso2  8573  unwdomg  8642  ac5num  9020  acni2  9030  fodomacn  9040  iundom2g  9525  fpwwe2lem3  9618  eltsk2g  9736  tskpwss  9737  tskpw  9738  tsken  9739  prlem934  10018  dedekindle  10364  ltord1  10717  leord1  10718  eqord1  10719  ltord2  10720  leord2  10721  eqord2  10722  supmul1  11155  seqcaopr2  13002  bccl  13274  hashbc  13400  limsupbnd2  14384  2clim  14473  climsup  14570  caurcvg2  14578  caucvgb  14580  isummulc2  14663  telfsumo2  14705  fsumparts  14708  incexclem  14738  isumshft  14741  climcndslem1  14751  climcndslem2  14752  supcvg  14758  geomulcvg  14777  mertenslem2  14787  mertens  14788  bpolycl  14953  bpolydif  14956  rpnnen2lem10  15122  dvdsprime  15573  iscatd2  16514  fuciso  16807  luble  17159  glble  17172  lubub  17291  lubl  17292  mgmlrid  17438  grpinvex  17604  issubg2  17781  issubg4  17785  nmzbi  17806  gagrpid  17898  cntzi  17933  psgnunilem2  18086  sylow1lem3  18186  pgpfi  18191  slwispgp  18197  sylow2alem1  18203  dprdfcl  18583  ablfac2  18659  abveq0  18999  issrngd  19034  psrbagconf1o  19547  pf1ind  19892  phllmhm  20150  ipcl  20151  ipeq0  20156  isphld  20172  ocvi  20186  cayhamlem3  20865  elcls3  21060  neindisj2  21100  perfi  21132  cnima  21242  1stcfb  21421  1stcelcls  21437  llyi  21450  nllyi  21451  locfinnei  21499  1stckgenlem  21529  ptbasin  21553  txcls  21580  ptcnp  21598  ufli  21890  tgpt0  22094  tsmsxplem2  22129  nrmmetd  22551  tngngp  22630  tngngp3  22632  reperflem  22793  lebnumlem3  22934  htpyi  22945  htpycc  22951  phtpyi  22955  cfili  23237  cmetcvg  23254  caubl  23277  caublcls  23278  bcthlem2  23293  bcthlem3  23294  bcthlem4  23295  ovolicc2lem1  23456  ovolicc2lem5  23460  ovolicc2  23461  voliunlem3  23491  volsuplem  23494  uniioombllem2  23522  mbfima  23569  ismbfd  23577  ismbf3d  23591  mbfmullem  23662  itg2monolem1  23687  itg2i1fseqle  23691  itg2i1fseq  23692  itg2i1fseq2  23693  itg2addlem  23695  bddmulibl  23775  c1liplem1  23929  dvfsumle  23954  dvfsumabs  23956  dvfsumrlimf  23958  dvfsumlem1  23959  dvfsumlem2  23960  dvfsumlem3  23961  dvfsumlem4  23962  dvfsumrlimge0  23963  dvfsum2  23967  ftc1lem6  23974  ulmcau  24319  ulmdvlem1  24324  ulmdvlem3  24326  mtestbdd  24329  itgulm  24332  radcnvlem1  24337  abelthlem5  24359  abelthlem7  24362  areambl  24855  2lgslem1a  25286  dchrisumlem2  25349  dchrvmasumiflem1  25360  pntpbnd1  25445  ostthlem1  25486  tglowdim1i  25566  brbtwn2  25955  ax5seglem1  25978  ax5seglem2  25979  ax5seglem9  25987  axcontlem4  26017  axcontlem12  26025  0vtxrusgr  26654  fusgreghash2wsp  27463  grpoidinvlem3  27640  grpoidinv  27642  grpoidinv2  27649  vcidOLD  27699  minvecolem5  28017  hcaucvg  28323  hlimconvi  28328  lnopeq0i  29146  cnlnadjlem5  29210  csmdsymi  29473  difelsiga  30476  eulerpartlemb  30710  ballotlemfc0  30834  ballotlemfcc  30835  ptpconn  31493  cvmsdisj  31530  cvmshmeo  31531  snmlflim  31592  elmrsubrn  31695  mvtinf  31730  sinccvg  31845  fnemeet1  32638  fnemeet2  32639  fnejoin1  32640  fnejoin2  32641  bj-seex  33196  poimirlem27  33718  poimirlem32  33723  mblfinlem1  33728  ovoliunnfl  33733  ex-ovoliunnfl  33734  voliunnfl  33735  volsupnfl  33736  mbfresfi  33738  itg2gt0cn  33747  bddiblnc  33762  ftc1cnnc  33766  ftc1anc  33775  upixp  33806  filbcmb  33817  sdclem1  33821  seqpo  33825  incsequz2  33827  mettrifi  33835  caushft  33839  sstotbnd2  33855  heibor1lem  33890  heiborlem3  33894  heiborlem10  33901  heibor  33902  rrndstprj2  33912  cmpidelt  33940  rngoid  33983  limsuc2  38082  cvgdvgrat  38983  cncmpmax  39659  foelrnf  39841  mccllem  40301  mccl  40302  climinf  40310  climsuse  40312  islptre  40323  limcperiod  40332  addlimc  40352  0ellimcdiv  40353  cncficcgt0  40573  fperdvper  40605  dvbdfbdioolem2  40616  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvnprodlem3  40635  stoweidlem7  40696  stoweidlem15  40704  stoweidlem21  40710  stoweidlem31  40720  stoweidlem35  40724  stoweidlem36  40725  stoweidlem50  40739  stoweidlem57  40746  stoweidlem59  40748  wallispilem3  40756  dirkercncflem2  40793  dirkercncflem4  40795  fourierdlem32  40828  fourierdlem33  40829  fourierdlem39  40835  fourierdlem62  40857  fourierdlem71  40866  fourierdlem89  40884  fourierdlem91  40886  fourierdlem93  40888  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  etransclem24  40947  etransclem32  40955  smflimlem6  41459  smfpimcc  41489  smfsuplem2  41493
  Copyright terms: Public domain W3C validator