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

Theorem rspccv 3275
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 3274 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32com12 32 1 (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  wral 2892
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 2032  ax-13 2229  ax-ext 2586
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 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-v 3171
This theorem is referenced by:  elinti  4411  trss  4680  fvn0ssdmfun  6240  dff3  6262  2fvcoidd  6427  ofrval  6779  limsuc  6915  limuni3  6918  frxp  7148  wfrdmcl  7284  smo11  7322  odi  7520  supub  8222  suplub  8223  elirrv  8361  dfom3  8401  noinfep  8414  oemapvali  8438  tcrank  8604  infxpenlem  8693  alephle  8768  dfac5lem5  8807  dfac2  8810  cofsmo  8948  coftr  8952  infpssrlem4  8985  isf34lem6  9059  axcc2lem  9115  domtriomlem  9121  axdc2lem  9127  axdc3lem2  9130  axdc4lem  9134  ac5b  9157  zorn2lem2  9176  zorn2lem6  9180  pwcfsdom  9258  inar1  9450  grupw  9470  grupr  9472  gruurn  9473  grothpw  9501  grothpwex  9502  axgroth6  9503  grothomex  9504  nqereu  9604  supsrlem  9785  axpre-sup  9843  dedekind  10048  dedekindle  10049  supmullem1  10837  supmul  10839  peano5nni  10867  dfnn2  10877  peano5uzi  11295  zindd  11307  1arith  15412  ramcl  15514  clatleglb  16892  pslem  16972  cygabl  18058  eqcoe1ply1eq  19431  psgndiflemA  19708  mvmumamul1  20118  smadiadetlem0  20225  chpscmat  20405  basis2  20505  tg2  20519  clsndisj  20628  cnpimaex  20809  t1sncld  20879  regsep  20887  nrmsep3  20908  cmpsub  20952  2ndc1stc  21003  refssex  21063  ptfinfin  21071  txcnpi  21160  txcmplem1  21193  tx1stc  21202  filss  21406  ufilss  21458  fclsopni  21568  fclsrest  21577  alexsubb  21599  alexsubALTlem2  21601  alexsubALTlem4  21603  ghmcnp  21667  qustgplem  21673  mopni  22045  metrest  22077  metcnpi  22097  metcnpi2  22098  cfilucfil  22112  nmolb  22260  nmoleub2lem2  22652  ovoliunlem1  22991  ovolicc2lem3  23008  mblsplit  23021  fta1b  23647  plycj  23751  mtest  23876  lgamgulmlem1  24469  sqfpc  24577  ostth2lem2  25037  ostth3  25041  vdiscusgra  26211  rusgranumwwlkl1  26236  usgn0fidegnn0  26319  numclwwlk1  26388  lpni  26485  nvz  26699  ubthlem2  26914  chcompl  27286  ocin  27342  hmopidmchi  28197  dmdmd  28346  dmdbr5  28354  mdsl1i  28367  sigaclci  29325  bnj23  29841  kur14lem9  30253  sconpht  30268  cvmsdisj  30309  untelirr  30642  untsucf  30644  dfon2lem4  30738  dfon2lem6  30740  dfon2lem7  30741  dfon2lem8  30742  dfon2  30744  frrlem5e  30835  sltval2  30856  fwddifnp1  31245  poimirlem18  32397  poimirlem21  32400  heibor1lem  32578  heiborlem4  32583  heiborlem6  32585  atlex  33421  psubspi  33851  elpcliN  33997  ldilval  34217  trlord  34675  tendotp  34867  hdmapval2  35942  pwelg  36684  gneispace0nelrn2  37259  gneispaceel2  37262  gneispacess2  37264  stoweid  38757  iccpartltu  39765  iccpartgtl  39766  iccpartleu  39768  iccpartgel  39769  nbgrnself2  40584  vdiscusgr  40746  rusgrnumwrdl2  40785  ewlkinedg  40805  av-numclwwlk1  41527
  Copyright terms: Public domain W3C validator