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

Theorem rspccv 3296
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 3295 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32com12 32 1 (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-v 3192
This theorem is referenced by:  elinti  4457  trss  4731  fvn0ssdmfun  6316  dff3  6338  2fvcoidd  6517  ofrval  6872  limsuc  7011  limuni3  7014  frxp  7247  wfrdmcl  7383  smo11  7421  odi  7619  supub  8325  suplub  8326  elirrv  8464  dfom3  8504  noinfep  8517  oemapvali  8541  tcrank  8707  infxpenlem  8796  alephle  8871  dfac5lem5  8910  dfac2  8913  cofsmo  9051  coftr  9055  infpssrlem4  9088  isf34lem6  9162  axcc2lem  9218  domtriomlem  9224  axdc2lem  9230  axdc3lem2  9233  axdc4lem  9237  ac5b  9260  zorn2lem2  9279  zorn2lem6  9283  pwcfsdom  9365  inar1  9557  grupw  9577  grupr  9579  gruurn  9580  grothpw  9608  grothpwex  9609  axgroth6  9610  grothomex  9611  nqereu  9711  supsrlem  9892  axpre-sup  9950  dedekind  10160  dedekindle  10161  supmullem1  10953  supmul  10955  peano5nni  10983  dfnn2  10993  peano5uzi  11426  zindd  11438  1arith  15574  ramcl  15676  clatleglb  17066  pslem  17146  cygabl  18232  eqcoe1ply1eq  19607  psgndiflemA  19887  mvmumamul1  20300  smadiadetlem0  20407  chpscmat  20587  basis2  20695  tg2  20709  clsndisj  20819  cnpimaex  21000  t1sncld  21070  regsep  21078  nrmsep3  21099  cmpsub  21143  2ndc1stc  21194  refssex  21254  ptfinfin  21262  txcnpi  21351  txcmplem1  21384  tx1stc  21393  filss  21597  ufilss  21649  fclsopni  21759  fclsrest  21768  alexsubb  21790  alexsubALTlem2  21792  alexsubALTlem4  21794  ghmcnp  21858  qustgplem  21864  mopni  22237  metrest  22269  metcnpi  22289  metcnpi2  22290  cfilucfil  22304  nmolb  22461  nmoleub2lem2  22856  ovoliunlem1  23210  ovolicc2lem3  23227  mblsplit  23240  fta1b  23867  plycj  23971  mtest  24096  lgamgulmlem1  24689  sqfpc  24797  ostth2lem2  25257  ostth3  25261  nbgrnself2  26180  vdiscusgr  26347  rusgrnumwrdl2  26386  ewlkinedg  26404  numclwwlk1  27120  l2p  27219  lpni  27220  nvz  27412  ubthlem2  27615  chcompl  27987  ocin  28043  hmopidmchi  28898  dmdmd  29047  dmdbr5  29055  mdsl1i  29068  sigaclci  30018  bnj23  30545  kur14lem9  30957  sconnpht  30972  cvmsdisj  31013  untelirr  31346  untsucf  31348  dfon2lem4  31445  dfon2lem6  31447  dfon2lem7  31448  dfon2lem8  31449  dfon2  31451  frrlem5e  31542  sltval2  31563  fwddifnp1  31967  poimirlem18  33098  poimirlem21  33101  heibor1lem  33279  heiborlem4  33284  heiborlem6  33286  atlex  34122  psubspi  34552  elpcliN  34698  ldilval  34918  trlord  35376  tendotp  35568  hdmapval2  36643  pwelg  37385  gneispace0nelrn2  37960  gneispaceel2  37963  gneispacess2  37965  stoweid  39617  iccpartltu  40689  iccpartgtl  40690  iccpartleu  40692  iccpartgel  40693  ssdifsn  41752
  Copyright terms: Public domain W3C validator