Theorem rspccv 3609

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

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3608	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3061

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  elinti  4959  trss  5276  fvn0ssdmfun  7076  dff3  7101  2fvcoidd  7297  ofrval  7684  limsuc  7840  limuni3  7843  peano5  7886  frxp  8114  wfrdmclOLD  8319  smo11  8366  odi  8581  supub  9456  suplub  9457  elirrv  9593  dfom3  9644  noinfep  9657  tcrank  9881  alephle  10085  dfac5lem5  10124  dfac2b  10127  cofsmo  10266  coftr  10270  infpssrlem4  10303  isf34lem6  10377  axcc2lem  10433  domtriomlem  10439  axdc2lem  10445  axdc3lem2  10448  axdc4lem  10452  ac5b  10475  zorn2lem2  10494  zorn2lem6  10498  pwcfsdom  10580  inar1  10772  grupw  10792  grupr  10794  gruurn  10795  grothpw  10823  grothpwex  10824  axgroth6  10825  grothomex  10826  nqereu  10926  supsrlem  11108  axpre-sup  11166  dedekind  11381  dedekindle  11382  supmullem1  12188  supmul  12190  peano5nni  12219  dfnn2  12229  peano5uzi  12655  zindd  12667  lcmfdvds  16583  lcmfunsn  16585  1arith  16864  ramcl  16966  clatleglb  18475  pslem  18529  cyccom  19118  rngisomring1  20359  psgndiflemA  21373  eqcoe1ply1eq  22041  mvmumamul1  22276  smadiadetlem0  22383  chpscmat  22564  basis2  22674  tg2  22688  clsndisj  22799  cnpimaex  22980  t1sncld  23050  regsep  23058  nrmsep3  23079  cmpsub  23124  2ndc1stc  23175  refssex  23235  ptfinfin  23243  txcnpi  23332  txcmplem1  23365  tx1stc  23374  filss  23577  ufilss  23629  fclsopni  23739  fclsrest  23748  alexsubb  23770  alexsubALTlem2  23772  alexsubALTlem4  23774  ghmcnp  23839  qustgplem  23845  mopni  24221  metrest  24253  metcnpi  24273  metcnpi2  24274  nmolb  24454  nmoleub2lem2  24856  ovoliunlem1  25243  ovolicc2lem3  25260  mblsplit  25273  fta1b  25911  plycj  26015  lgamgulmlem1  26757  sqfpc  26865  ostth2lem2  27361  ostth3  27365  sltval2  27383  nogt01o  27423  madebdayim  27607  madebdaylemlrcut  27618  precsexlem9  27888  peano5n0s  27923  dfn0s2  27929  vdiscusgr  29043  0vtxrusgr  29089  rusgrnumwrdl2  29098  ewlkinedg  29116  eupthseg  29714  upgreupthseg  29717  numclwwlk1  29869  l2p  29987  lpni  29988  nvz  30177  chcompl  30750  ocin  30804  hmopidmchi  31659  dmdmd  31808  dmdbr5  31816  mdsl1i  31829  sigaclci  33416  bnj23  34015  kur14lem9  34491  sconnpht  34506  cvmsdisj  34547  sat1el2xp  34656  untelirr  34969  untsucf  34971  dfon2lem4  35050  dfon2lem6  35052  dfon2lem7  35053  dfon2lem8  35054  dfon2  35056  fwddifnp1  35429  domalom  36588  pibt2  36601  poimirlem18  36809  poimirlem21  36812  heibor1lem  36980  heiborlem4  36985  heiborlem6  36987  atlex  38489  psubspi  38921  elpcliN  39067  ldilval  39287  trlord  39743  tendotp  39935  hdmapval2  41006  cantnfresb  42376  pwelg  42613  gneispace0nelrn2  43194  gneispaceel2  43197  gneispacess2  43199  stoweid  45078  iccpartimp  46384  iccpartltu  46392  iccpartgtl  46393  iccpartleu  46395  iccpartgel  46396  isomushgr  46793  isomuspgrlem1  46794  isomuspgr  46801  isomgrtrlem  46805  1arymaptf1  47416