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

Theorem rspccva 3281
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 3278 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 445 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175
This theorem is referenced by:  disjne  3974  seex  5001  preddowncl  5624  foelrn  6286  grprinvlem  6770  caofid0l  6823  caofid0r  6824  caofid1  6825  caofid2  6826  onnseq  7328  odi  7546  omsmolem  7620  fvixp  7799  unblem1  8097  ordiso2  8303  unwdomg  8372  ac5num  8742  acni2  8752  fodomacn  8762  iundom2g  9241  fpwwe2lem3  9334  eltsk2g  9452  tskpwss  9453  tskpw  9454  tsken  9455  prlem934  9734  dedekindle  10080  ltord1  10433  leord1  10434  eqord1  10435  ltord2  10436  leord2  10437  eqord2  10438  supmul1  10869  seqcaopr2  12699  bccl  12971  hashbc  13094  limsupbnd2  14062  2clim  14151  climsup  14248  caurcvg2  14256  caucvgb  14258  isummulc2  14335  telfsumo2  14376  fsumparts  14379  incexclem  14407  isumshft  14410  climcndslem1  14420  climcndslem2  14421  supcvg  14427  geomulcvg  14446  mertenslem2  14456  mertens  14457  bpolycl  14622  bpolydif  14625  rpnnen2lem10  14791  dvdsprime  15238  iscatd2  16165  fuciso  16458  luble  16810  glble  16823  lubub  16942  lubl  16943  mgmlrid  17089  grpinvex  17255  issubg2  17432  issubg4  17436  nmzbi  17457  gagrpid  17550  cntzi  17585  psgnunilem2  17738  sylow1lem3  17838  pgpfi  17843  slwispgp  17849  sylow2alem1  17855  dprdfcl  18235  ablfac2  18311  abveq0  18649  issrngd  18684  psrbagconf1o  19195  pf1ind  19540  phllmhm  19796  ipcl  19797  ipeq0  19802  isphld  19818  ocvi  19832  cayhamlem3  20511  elcls3  20697  neindisj2  20737  perfi  20769  cnima  20879  1stcfb  21058  1stcelcls  21074  llyi  21087  nllyi  21088  locfinnei  21136  1stckgenlem  21166  ptbasin  21190  txcls  21217  ptcnp  21235  ufli  21528  tgpt0  21732  tsmsxplem2  21767  nrmmetd  22189  tngngp  22268  tngngp3  22270  reperflem  22429  lebnumlem3  22570  htpyi  22581  htpycc  22587  phtpyi  22591  cfili  22874  cmetcvg  22891  caubl  22914  caublcls  22915  bcthlem2  22930  bcthlem3  22931  bcthlem4  22932  ovolicc2lem1  23092  ovolicc2lem5  23096  ovolicc2  23097  voliunlem3  23127  volsuplem  23130  uniioombllem2  23157  mbfima  23205  ismbfd  23213  ismbf3d  23227  mbfmullem  23298  itg2monolem1  23323  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  bddmulibl  23411  c1liplem1  23563  dvfsumle  23588  dvfsumabs  23590  dvfsumrlimf  23592  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlimge0  23597  dvfsum2  23601  ftc1lem6  23608  ulmcau  23953  ulmdvlem1  23958  ulmdvlem3  23960  mtestbdd  23963  itgulm  23966  radcnvlem1  23971  abelthlem5  23993  abelthlem7  23996  areambl  24485  2lgslem1a  24916  dchrisumlem2  24979  dchrvmasumiflem1  24990  pntpbnd1  25075  ostthlem1  25116  tglowdim1i  25196  brbtwn2  25585  ax5seglem1  25608  ax5seglem2  25609  ax5seglem9  25617  axcontlem4  25647  axcontlem12  25655  usgrcyclnl1  26168  eupaseg  26500  usgreghash2spot  26596  grpoidinvlem3  26744  grpoidinv  26746  grpoidinv2  26753  vcidOLD  26803  minvecolem5  27121  hcaucvg  27427  hlimconvi  27432  lnopeq0i  28250  cnlnadjlem5  28314  csmdsymi  28577  difelsiga  29523  eulerpartlemb  29757  ballotlemfc0  29881  ballotlemfcc  29882  ptpcon  30469  cvmsdisj  30506  cvmshmeo  30507  snmlflim  30568  elmrsubrn  30671  mvtinf  30706  sinccvg  30821  fnemeet1  31531  fnemeet2  31532  fnejoin1  31533  fnejoin2  31534  bj-seex  32111  poimirlem27  32606  poimirlem32  32611  mblfinlem1  32616  ovoliunnfl  32621  ex-ovoliunnfl  32622  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  itg2gt0cn  32635  bddiblnc  32650  ftc1cnnc  32654  ftc1anc  32663  upixp  32694  filbcmb  32705  sdclem1  32709  seqpo  32713  incsequz2  32715  mettrifi  32723  caushft  32727  sstotbnd2  32743  heibor1lem  32778  heiborlem3  32782  heiborlem10  32789  heibor  32790  rrndstprj2  32800  cmpidelt  32828  rngoid  32871  limsuc2  36629  cvgdvgrat  37534  cncmpmax  38214  foelrnf  38368  mccllem  38664  mccl  38665  climinf  38673  climsuse  38675  islptre  38686  limcperiod  38695  addlimc  38715  0ellimcdiv  38716  cncficcgt0  38774  fperdvper  38808  dvbdfbdioolem2  38819  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem3  38838  stoweidlem7  38900  stoweidlem15  38908  stoweidlem21  38914  stoweidlem31  38924  stoweidlem35  38928  stoweidlem36  38929  stoweidlem50  38943  stoweidlem57  38950  stoweidlem59  38952  wallispilem3  38960  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem32  39032  fourierdlem33  39033  fourierdlem39  39039  fourierdlem62  39061  fourierdlem71  39070  fourierdlem89  39088  fourierdlem91  39090  fourierdlem93  39092  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  etransclem24  39151  etransclem32  39159  smflimlem6  39662  0vtxrusgr  40777  fusgreghash2wsp  41502
  Copyright terms: Public domain W3C validator