Theorem rspccv 3602

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 3601	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051

This theorem is referenced by:  elinti  4935  trss  5250  fvn0ssdmfun  7074  dff3  7100  2fvcoidd  7299  ofrval  7691  limsuc  7852  limuni3  7855  peano5  7897  frxp  8133  wfrdmclOLD  8339  smo11  8386  odi  8599  supub  9481  suplub  9482  elirrv  9618  dfom3  9669  noinfep  9682  tcrank  9906  alephle  10110  dfac5lem5  10149  dfac2b  10153  cofsmo  10291  coftr  10295  infpssrlem4  10328  isf34lem6  10402  axcc2lem  10458  domtriomlem  10464  axdc2lem  10470  axdc3lem2  10473  axdc4lem  10477  ac5b  10500  zorn2lem2  10519  zorn2lem6  10523  pwcfsdom  10605  inar1  10797  grupw  10817  grupr  10819  gruurn  10820  grothpw  10848  grothpwex  10849  axgroth6  10850  grothomex  10851  nqereu  10951  supsrlem  11133  axpre-sup  11191  dedekind  11406  dedekindle  11407  supmullem1  12220  supmul  12222  peano5nni  12251  dfnn2  12261  peano5uzi  12690  zindd  12702  lcmfdvds  16661  lcmfunsn  16663  1arith  16947  ramcl  17049  clatleglb  18532  pslem  18586  cyccom  19190  rngisomring1  20436  psgndiflemA  21573  eqcoe1ply1eq  22251  mvmumamul1  22508  smadiadetlem0  22615  chpscmat  22796  basis2  22905  tg2  22919  clsndisj  23029  cnpimaex  23210  t1sncld  23280  regsep  23288  nrmsep3  23309  cmpsub  23354  2ndc1stc  23405  refssex  23465  ptfinfin  23473  txcnpi  23562  txcmplem1  23595  tx1stc  23604  filss  23807  ufilss  23859  fclsopni  23969  fclsrest  23978  alexsubb  24000  alexsubALTlem2  24002  alexsubALTlem4  24004  ghmcnp  24069  qustgplem  24075  mopni  24449  metrest  24481  metcnpi  24501  metcnpi2  24502  nmolb  24674  nmoleub2lem2  25085  ovoliunlem1  25473  ovolicc2lem3  25490  mblsplit  25503  fta1b  26147  plycj  26253  plycjOLD  26255  lgamgulmlem1  27008  sqfpc  27116  ostth2lem2  27614  ostth3  27618  sltval2  27637  nogt01o  27677  madebdayim  27862  madebdaylemlrcut  27873  precsexlem9  28175  dfn0s2  28272  peano5uzs  28326  vdiscusgr  29477  0vtxrusgr  29523  rusgrnumwrdl2  29532  ewlkinedg  29550  eupthseg  30153  upgreupthseg  30156  numclwwlk1  30308  l2p  30426  lpni  30427  nvz  30616  chcompl  31189  ocin  31243  hmopidmchi  32098  dmdmd  32247  dmdbr5  32255  mdsl1i  32268  sigaclci  34092  bnj23  34691  kur14lem9  35178  sconnpht  35193  cvmsdisj  35234  sat1el2xp  35343  untelirr  35667  untsucf  35669  dfon2lem4  35746  dfon2lem6  35748  dfon2lem7  35749  dfon2lem8  35750  dfon2  35752  fwddifnp1  36125  domalom  37364  pibt2  37377  poimirlem18  37604  poimirlem21  37607  heibor1lem  37775  heiborlem4  37780  heiborlem6  37782  atlex  39276  psubspi  39708  elpcliN  39854  ldilval  40074  trlord  40530  tendotp  40722  hdmapval2  41793  cantnfresb  43299  pwelg  43535  gneispace0nelrn2  44116  gneispaceel2  44119  gneispacess2  44121  stoweid  46035  iccpartimp  47362  iccpartltu  47370  iccpartgtl  47371  iccpartleu  47373  iccpartgel  47374  isuspgrim0  47830  gricushgr  47844  1arymaptf1  48521