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

Theorem rspccv 3510
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 3509 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32com12 32 1 (∀𝑥𝐵 𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2157  wral 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-v 3404
This theorem is referenced by:  ssdifsnOLD  4521  elinti  4689  trss  4966  fvn0ssdmfun  6582  dff3  6604  2fvcoidd  6786  ofrval  7147  limsuc  7289  limuni3  7292  frxp  7531  wfrdmcl  7669  smo11  7707  odi  7906  supub  8614  suplub  8615  elirrv  8750  dfom3  8801  noinfep  8814  tcrank  9004  alephle  9204  dfac5lem5  9243  dfac2b  9246  dfac2OLD  9248  cofsmo  9386  coftr  9390  infpssrlem4  9423  isf34lem6  9497  axcc2lem  9553  domtriomlem  9559  axdc2lem  9565  axdc3lem2  9568  axdc4lem  9572  ac5b  9595  zorn2lem2  9614  zorn2lem6  9618  pwcfsdom  9700  inar1  9892  grupw  9912  grupr  9914  gruurn  9915  grothpw  9943  grothpwex  9944  axgroth6  9945  grothomex  9946  nqereu  10046  supsrlem  10227  axpre-sup  10285  dedekind  10495  dedekindle  10496  supmullem1  11288  supmul  11290  peano5nni  11318  dfnn2  11330  peano5uzi  11752  zindd  11764  1arith  15868  ramcl  15970  clatleglb  17351  pslem  17431  cygabl  18513  eqcoe1ply1eq  19895  psgndiflemA  20175  mvmumamul1  20592  smadiadetlem0  20700  chpscmat  20881  basis2  20990  tg2  21004  clsndisj  21114  cnpimaex  21295  t1sncld  21365  regsep  21373  nrmsep3  21394  cmpsub  21438  2ndc1stc  21489  refssex  21549  ptfinfin  21557  txcnpi  21646  txcmplem1  21679  tx1stc  21688  filss  21891  ufilss  21943  fclsopni  22053  fclsrest  22062  alexsubb  22084  alexsubALTlem2  22086  alexsubALTlem4  22088  ghmcnp  22152  qustgplem  22158  mopni  22531  metrest  22563  metcnpi  22583  metcnpi2  22584  nmolb  22755  nmoleub2lem2  23149  ovoliunlem1  23506  ovolicc2lem3  23523  mblsplit  23536  fta1b  24166  plycj  24270  lgamgulmlem1  24992  sqfpc  25100  ostth2lem2  25560  ostth3  25564  nbgrnself2OLD  26498  vdiscusgr  26678  rusgrnumwrdl2  26733  ewlkinedg  26751  numclwwlk1  27564  l2p  27685  lpni  27686  nvz  27875  chcompl  28450  ocin  28506  hmopidmchi  29361  dmdmd  29510  dmdbr5  29518  mdsl1i  29531  sigaclci  30543  bnj23  31132  kur14lem9  31541  sconnpht  31556  cvmsdisj  31597  untelirr  31929  untsucf  31931  dfon2lem4  32033  dfon2lem6  32035  dfon2lem7  32036  dfon2lem8  32037  dfon2  32039  frrlem5e  32131  sltval2  32152  fwddifnp1  32615  poimirlem18  33759  poimirlem21  33762  heibor1lem  33938  heiborlem4  33943  heiborlem6  33945  atlex  35115  psubspi  35546  elpcliN  35692  ldilval  35912  trlord  36368  tendotp  36560  hdmapval2  37631  pwelg  38383  gneispace0nelrn2  38957  gneispaceel2  38960  gneispacess2  38962  stoweid  40777  iccpartltu  41954  iccpartgtl  41955  iccpartleu  41957  iccpartgel  41958
  Copyright terms: Public domain W3C validator