Theorem rspccv 3598

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  elinti  4931  trss  5240  fvn0ssdmfun  7063  dff3  7089  2fvcoidd  7289  ofrval  7681  limsuc  7842  limuni3  7845  peano5  7887  frxp  8123  wfrdmclOLD  8329  smo11  8376  odi  8589  supub  9469  suplub  9470  elirrv  9608  dfom3  9659  noinfep  9672  tcrank  9896  alephle  10100  dfac5lem5  10139  dfac2b  10143  cofsmo  10281  coftr  10285  infpssrlem4  10318  isf34lem6  10392  axcc2lem  10448  domtriomlem  10454  axdc2lem  10460  axdc3lem2  10463  axdc4lem  10467  ac5b  10490  zorn2lem2  10509  zorn2lem6  10513  pwcfsdom  10595  inar1  10787  grupw  10807  grupr  10809  gruurn  10810  grothpw  10838  grothpwex  10839  axgroth6  10840  grothomex  10841  nqereu  10941  supsrlem  11123  axpre-sup  11181  dedekind  11396  dedekindle  11397  supmullem1  12210  supmul  12212  peano5nni  12241  dfnn2  12251  peano5uzi  12680  zindd  12692  lcmfdvds  16659  lcmfunsn  16661  1arith  16945  ramcl  17047  clatleglb  18526  pslem  18580  cyccom  19184  rngisomring1  20426  psgndiflemA  21559  eqcoe1ply1eq  22235  mvmumamul1  22490  smadiadetlem0  22597  chpscmat  22778  basis2  22887  tg2  22901  clsndisj  23011  cnpimaex  23192  t1sncld  23262  regsep  23270  nrmsep3  23291  cmpsub  23336  2ndc1stc  23387  refssex  23447  ptfinfin  23455  txcnpi  23544  txcmplem1  23577  tx1stc  23586  filss  23789  ufilss  23841  fclsopni  23951  fclsrest  23960  alexsubb  23982  alexsubALTlem2  23984  alexsubALTlem4  23986  ghmcnp  24051  qustgplem  24057  mopni  24429  metrest  24461  metcnpi  24481  metcnpi2  24482  nmolb  24654  nmoleub2lem2  25065  ovoliunlem1  25453  ovolicc2lem3  25470  mblsplit  25483  fta1b  26127  plycj  26233  plycjOLD  26235  lgamgulmlem1  26989  sqfpc  27097  ostth2lem2  27595  ostth3  27599  sltval2  27618  nogt01o  27658  madebdayim  27843  madebdaylemlrcut  27854  precsexlem9  28156  dfn0s2  28253  peano5uzs  28307  vdiscusgr  29457  0vtxrusgr  29503  rusgrnumwrdl2  29512  ewlkinedg  29530  eupthseg  30133  upgreupthseg  30136  numclwwlk1  30288  l2p  30406  lpni  30407  nvz  30596  chcompl  31169  ocin  31223  hmopidmchi  32078  dmdmd  32227  dmdbr5  32235  mdsl1i  32248  sigaclci  34109  bnj23  34695  kur14lem9  35182  sconnpht  35197  cvmsdisj  35238  sat1el2xp  35347  untelirr  35671  untsucf  35673  dfon2lem4  35750  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  fwddifnp1  36129  domalom  37368  pibt2  37381  poimirlem18  37608  poimirlem21  37611  heibor1lem  37779  heiborlem4  37784  heiborlem6  37786  atlex  39280  psubspi  39712  elpcliN  39858  ldilval  40078  trlord  40534  tendotp  40726  hdmapval2  41797  cantnfresb  43295  pwelg  43531  gneispace0nelrn2  44112  gneispaceel2  44115  gneispacess2  44117  stoweid  46040  iccpartimp  47379  iccpartltu  47387  iccpartgtl  47388  iccpartleu  47390  iccpartgel  47391  isuspgrim0  47855  gricushgr  47878  1arymaptf1  48570