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

Theorem rspccv 3576
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspccv (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccv
StepHypRef Expression
1 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
21rspcv 3575 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32com12 32 1 (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063
This theorem is referenced by:  elinti  4914  trss  5231  fvn0ssdmfun  7022  dff3  7046  2fvcoidd  7239  ofrval  7625  limsuc  7781  limuni3  7784  peano5  7826  frxp  8054  wfrdmclOLD  8259  smo11  8306  odi  8522  supub  9391  suplub  9392  elirrv  9528  dfom3  9579  noinfep  9592  tcrank  9816  alephle  10020  dfac5lem5  10059  dfac2b  10062  cofsmo  10201  coftr  10205  infpssrlem4  10238  isf34lem6  10312  axcc2lem  10368  domtriomlem  10374  axdc2lem  10380  axdc3lem2  10383  axdc4lem  10387  ac5b  10410  zorn2lem2  10429  zorn2lem6  10433  pwcfsdom  10515  inar1  10707  grupw  10727  grupr  10729  gruurn  10730  grothpw  10758  grothpwex  10759  axgroth6  10760  grothomex  10761  nqereu  10861  supsrlem  11043  axpre-sup  11101  dedekind  11314  dedekindle  11315  supmullem1  12121  supmul  12123  peano5nni  12152  dfnn2  12162  peano5uzi  12588  zindd  12600  lcmfdvds  16510  lcmfunsn  16512  1arith  16791  ramcl  16893  clatleglb  18399  pslem  18453  cyccom  18987  psgndiflemA  20990  eqcoe1ply1eq  21652  mvmumamul1  21887  smadiadetlem0  21994  chpscmat  22175  basis2  22285  tg2  22299  clsndisj  22410  cnpimaex  22591  t1sncld  22661  regsep  22669  nrmsep3  22690  cmpsub  22735  2ndc1stc  22786  refssex  22846  ptfinfin  22854  txcnpi  22943  txcmplem1  22976  tx1stc  22985  filss  23188  ufilss  23240  fclsopni  23350  fclsrest  23359  alexsubb  23381  alexsubALTlem2  23383  alexsubALTlem4  23385  ghmcnp  23450  qustgplem  23456  mopni  23832  metrest  23864  metcnpi  23884  metcnpi2  23885  nmolb  24065  nmoleub2lem2  24463  ovoliunlem1  24850  ovolicc2lem3  24867  mblsplit  24880  fta1b  25518  plycj  25622  lgamgulmlem1  26362  sqfpc  26470  ostth2lem2  26966  ostth3  26970  sltval2  26988  nogt01o  27028  madebdayim  27201  madebdaylemlrcut  27212  vdiscusgr  28365  0vtxrusgr  28411  rusgrnumwrdl2  28420  ewlkinedg  28438  eupthseg  29036  upgreupthseg  29039  numclwwlk1  29191  l2p  29307  lpni  29308  nvz  29497  chcompl  30070  ocin  30124  hmopidmchi  30979  dmdmd  31128  dmdbr5  31136  mdsl1i  31149  sigaclci  32600  bnj23  33199  kur14lem9  33677  sconnpht  33692  cvmsdisj  33733  sat1el2xp  33842  untelirr  34148  untsucf  34150  dfon2lem4  34231  dfon2lem6  34233  dfon2lem7  34234  dfon2lem8  34235  dfon2  34237  fwddifnp1  34717  domalom  35842  pibt2  35855  poimirlem18  36063  poimirlem21  36066  heibor1lem  36235  heiborlem4  36240  heiborlem6  36242  atlex  37745  psubspi  38177  elpcliN  38323  ldilval  38543  trlord  38999  tendotp  39191  hdmapval2  40262  cantnfresb  41596  pwelg  41774  gneispace0nelrn2  42355  gneispaceel2  42358  gneispacess2  42360  stoweid  44236  iccpartimp  45541  iccpartltu  45549  iccpartgtl  45550  iccpartleu  45552  iccpartgel  45553  isomushgr  45950  isomuspgrlem1  45951  isomuspgr  45958  isomgrtrlem  45962  1arymaptf1  46660
  Copyright terms: Public domain W3C validator