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

Theorem rspccv 3606
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 3604 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32com12 32 1 (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  wral 3133
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-ral 3138
This theorem is referenced by:  elinti  4871  trss  5167  fvn0ssdmfun  6833  dff3  6857  2fvcoidd  7045  ofrval  7413  limsuc  7558  limuni3  7561  frxp  7816  wfrdmcl  7959  smo11  7997  odi  8201  supub  8920  suplub  8921  elirrv  9057  dfom3  9107  noinfep  9120  tcrank  9310  alephle  9512  dfac5lem5  9551  dfac2b  9554  cofsmo  9689  coftr  9693  infpssrlem4  9726  isf34lem6  9800  axcc2lem  9856  domtriomlem  9862  axdc2lem  9868  axdc3lem2  9871  axdc4lem  9875  ac5b  9898  zorn2lem2  9917  zorn2lem6  9921  pwcfsdom  10003  inar1  10195  grupw  10215  grupr  10217  gruurn  10218  grothpw  10246  grothpwex  10247  axgroth6  10248  grothomex  10249  nqereu  10349  supsrlem  10531  axpre-sup  10589  dedekind  10801  dedekindle  10802  supmullem1  11607  supmul  11609  peano5nni  11637  dfnn2  11647  peano5uzi  12068  zindd  12080  lcmfdvds  15984  lcmfunsn  15986  1arith  16261  ramcl  16363  clatleglb  17736  pslem  17816  cyccom  18346  cygablOLD  19011  eqcoe1ply1eq  20465  psgndiflemA  20745  mvmumamul1  21163  smadiadetlem0  21270  chpscmat  21450  basis2  21559  tg2  21573  clsndisj  21683  cnpimaex  21864  t1sncld  21934  regsep  21942  nrmsep3  21963  cmpsub  22008  2ndc1stc  22059  refssex  22119  ptfinfin  22127  txcnpi  22216  txcmplem1  22249  tx1stc  22258  filss  22461  ufilss  22513  fclsopni  22623  fclsrest  22632  alexsubb  22654  alexsubALTlem2  22656  alexsubALTlem4  22658  ghmcnp  22723  qustgplem  22729  mopni  23102  metrest  23134  metcnpi  23154  metcnpi2  23155  nmolb  23326  nmoleub2lem2  23724  ovoliunlem1  24109  ovolicc2lem3  24126  mblsplit  24139  fta1b  24773  plycj  24877  lgamgulmlem1  25617  sqfpc  25725  ostth2lem2  26221  ostth3  26225  vdiscusgr  27324  0vtxrusgr  27370  rusgrnumwrdl2  27379  ewlkinedg  27397  eupthseg  27994  upgreupthseg  27997  numclwwlk1  28149  l2p  28265  lpni  28266  nvz  28455  chcompl  29028  ocin  29082  hmopidmchi  29937  dmdmd  30086  dmdbr5  30094  mdsl1i  30107  sigaclci  31448  bnj23  32045  kur14lem9  32518  sconnpht  32533  cvmsdisj  32574  sat1el2xp  32683  untelirr  32991  untsucf  32993  dfon2lem4  33088  dfon2lem6  33090  dfon2lem7  33091  dfon2lem8  33092  dfon2  33094  sltval2  33220  fwddifnp1  33683  domalom  34766  pibt2  34779  poimirlem18  35020  poimirlem21  35023  heibor1lem  35192  heiborlem4  35197  heiborlem6  35199  atlex  36557  psubspi  36988  elpcliN  37134  ldilval  37354  trlord  37810  tendotp  38002  hdmapval2  39073  pwelg  40175  gneispace0nelrn2  40763  gneispaceel2  40766  gneispacess2  40768  stoweid  42631  iccpartimp  43860  iccpartltu  43868  iccpartgtl  43869  iccpartleu  43871  iccpartgel  43872  isomushgr  44270  isomuspgrlem1  44271  isomuspgr  44278  isomgrtrlem  44282  1arymaptf1  44982
  Copyright terms: Public domain W3C validator