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

Theorem rspccva 3339
 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 3336 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 445 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233 This theorem is referenced by:  disjne  4055  n0snor2el  4396  seex  5106  preddowncl  5745  foelrn  6418  grprinvlem  6914  caofid0l  6967  caofid0r  6968  caofid1  6969  caofid2  6970  onnseq  7486  odi  7704  omsmolem  7778  fvixp  7955  unblem1  8253  ordiso2  8461  unwdomg  8530  ac5num  8897  acni2  8907  fodomacn  8917  iundom2g  9400  fpwwe2lem3  9493  eltsk2g  9611  tskpwss  9612  tskpw  9613  tsken  9614  prlem934  9893  dedekindle  10239  ltord1  10592  leord1  10593  eqord1  10594  ltord2  10595  leord2  10596  eqord2  10597  supmul1  11030  seqcaopr2  12877  bccl  13149  hashbc  13275  limsupbnd2  14258  2clim  14347  climsup  14444  caurcvg2  14452  caucvgb  14454  isummulc2  14537  telfsumo2  14579  fsumparts  14582  incexclem  14612  isumshft  14615  climcndslem1  14625  climcndslem2  14626  supcvg  14632  geomulcvg  14651  mertenslem2  14661  mertens  14662  bpolycl  14827  bpolydif  14830  rpnnen2lem10  14996  dvdsprime  15447  iscatd2  16389  fuciso  16682  luble  17034  glble  17047  lubub  17166  lubl  17167  mgmlrid  17313  grpinvex  17479  issubg2  17656  issubg4  17660  nmzbi  17681  gagrpid  17773  cntzi  17808  psgnunilem2  17961  sylow1lem3  18061  pgpfi  18066  slwispgp  18072  sylow2alem1  18078  dprdfcl  18458  ablfac2  18534  abveq0  18874  issrngd  18909  psrbagconf1o  19422  pf1ind  19767  phllmhm  20025  ipcl  20026  ipeq0  20031  isphld  20047  ocvi  20061  cayhamlem3  20740  elcls3  20935  neindisj2  20975  perfi  21007  cnima  21117  1stcfb  21296  1stcelcls  21312  llyi  21325  nllyi  21326  locfinnei  21374  1stckgenlem  21404  ptbasin  21428  txcls  21455  ptcnp  21473  ufli  21765  tgpt0  21969  tsmsxplem2  22004  nrmmetd  22426  tngngp  22505  tngngp3  22507  reperflem  22668  lebnumlem3  22809  htpyi  22820  htpycc  22826  phtpyi  22830  cfili  23112  cmetcvg  23129  caubl  23152  caublcls  23153  bcthlem2  23168  bcthlem3  23169  bcthlem4  23170  ovolicc2lem1  23331  ovolicc2lem5  23335  ovolicc2  23336  voliunlem3  23366  volsuplem  23369  uniioombllem2  23397  mbfima  23444  ismbfd  23452  ismbf3d  23466  mbfmullem  23537  itg2monolem1  23562  itg2i1fseqle  23566  itg2i1fseq  23567  itg2i1fseq2  23568  itg2addlem  23570  bddmulibl  23650  c1liplem1  23804  dvfsumle  23829  dvfsumabs  23831  dvfsumrlimf  23833  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlimge0  23838  dvfsum2  23842  ftc1lem6  23849  ulmcau  24194  ulmdvlem1  24199  ulmdvlem3  24201  mtestbdd  24204  itgulm  24207  radcnvlem1  24212  abelthlem5  24234  abelthlem7  24237  areambl  24730  2lgslem1a  25161  dchrisumlem2  25224  dchrvmasumiflem1  25235  pntpbnd1  25320  ostthlem1  25361  tglowdim1i  25441  brbtwn2  25830  ax5seglem1  25853  ax5seglem2  25854  ax5seglem9  25862  axcontlem4  25892  axcontlem12  25900  0vtxrusgr  26529  fusgreghash2wsp  27318  grpoidinvlem3  27488  grpoidinv  27490  grpoidinv2  27497  vcidOLD  27547  minvecolem5  27865  hcaucvg  28171  hlimconvi  28176  lnopeq0i  28994  cnlnadjlem5  29058  csmdsymi  29321  difelsiga  30324  eulerpartlemb  30558  ballotlemfc0  30682  ballotlemfcc  30683  ptpconn  31341  cvmsdisj  31378  cvmshmeo  31379  snmlflim  31440  elmrsubrn  31543  mvtinf  31578  sinccvg  31693  fnemeet1  32486  fnemeet2  32487  fnejoin1  32488  fnejoin2  32489  bj-seex  33044  poimirlem27  33566  poimirlem32  33571  mblfinlem1  33576  ovoliunnfl  33581  ex-ovoliunnfl  33582  voliunnfl  33583  volsupnfl  33584  mbfresfi  33586  itg2gt0cn  33595  bddiblnc  33610  ftc1cnnc  33614  ftc1anc  33623  upixp  33654  filbcmb  33665  sdclem1  33669  seqpo  33673  incsequz2  33675  mettrifi  33683  caushft  33687  sstotbnd2  33703  heibor1lem  33738  heiborlem3  33742  heiborlem10  33749  heibor  33750  rrndstprj2  33760  cmpidelt  33788  rngoid  33831  limsuc2  37928  cvgdvgrat  38829  cncmpmax  39505  foelrnf  39687  mccllem  40147  mccl  40148  climinf  40156  climsuse  40158  islptre  40169  limcperiod  40178  addlimc  40198  0ellimcdiv  40199  cncficcgt0  40419  fperdvper  40451  dvbdfbdioolem2  40462  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem3  40481  stoweidlem7  40542  stoweidlem15  40550  stoweidlem21  40556  stoweidlem31  40566  stoweidlem35  40570  stoweidlem36  40571  stoweidlem50  40585  stoweidlem57  40592  stoweidlem59  40594  wallispilem3  40602  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem32  40674  fourierdlem33  40675  fourierdlem39  40681  fourierdlem62  40703  fourierdlem71  40712  fourierdlem89  40730  fourierdlem91  40732  fourierdlem93  40734  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  etransclem24  40793  etransclem32  40801  smflimlem6  41305  smfpimcc  41335  smfsuplem2  41339
 Copyright terms: Public domain W3C validator