Theorem rspccv 3576

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  elinti  4908  trss  5212  fvn0ssdmfun  7012  dff3  7038  2fvcoidd  7238  ofrval  7629  limsuc  7789  limuni3  7792  peano5  7833  frxp  8066  smo11  8294  odi  8504  supub  9368  suplub  9369  elirrvOLD  9509  dfom3  9562  noinfep  9575  tcrank  9799  alephle  10001  dfac5lem5  10040  dfac2b  10044  cofsmo  10182  coftr  10186  infpssrlem4  10219  isf34lem6  10293  axcc2lem  10349  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc4lem  10368  ac5b  10391  zorn2lem2  10410  zorn2lem6  10414  pwcfsdom  10496  inar1  10688  grupw  10708  grupr  10710  gruurn  10711  grothpw  10739  grothpwex  10740  axgroth6  10741  grothomex  10742  nqereu  10842  supsrlem  11024  axpre-sup  11082  dedekind  11298  dedekindle  11299  supmullem1  12114  supmul  12116  peano5nni  12150  dfnn2  12160  peano5uzi  12584  zindd  12596  lcmfdvds  16572  lcmfunsn  16574  1arith  16858  ramcl  16960  clatleglb  18443  pslem  18497  cyccom  19101  rngisomring1  20372  psgndiflemA  21527  eqcoe1ply1eq  22203  mvmumamul1  22458  smadiadetlem0  22565  chpscmat  22746  basis2  22855  tg2  22869  clsndisj  22979  cnpimaex  23160  t1sncld  23230  regsep  23238  nrmsep3  23259  cmpsub  23304  2ndc1stc  23355  refssex  23415  ptfinfin  23423  txcnpi  23512  txcmplem1  23545  tx1stc  23554  filss  23757  ufilss  23809  fclsopni  23919  fclsrest  23928  alexsubb  23950  alexsubALTlem2  23952  alexsubALTlem4  23954  ghmcnp  24019  qustgplem  24025  mopni  24397  metrest  24429  metcnpi  24449  metcnpi2  24450  nmolb  24622  nmoleub2lem2  25033  ovoliunlem1  25420  ovolicc2lem3  25437  mblsplit  25450  fta1b  26094  plycj  26200  plycjOLD  26202  lgamgulmlem1  26956  sqfpc  27064  ostth2lem2  27562  ostth3  27566  sltval2  27585  nogt01o  27625  madebdayim  27821  madebdaylemlrcut  27832  precsexlem9  28141  onsiso  28193  bdayon  28197  dfn0s2  28248  onsfi  28271  peano5uzs  28316  vdiscusgr  29496  0vtxrusgr  29542  rusgrnumwrdl2  29551  ewlkinedg  29569  eupthseg  30169  upgreupthseg  30172  numclwwlk1  30324  l2p  30442  lpni  30443  nvz  30632  chcompl  31205  ocin  31259  hmopidmchi  32114  dmdmd  32263  dmdbr5  32271  mdsl1i  32284  sigaclci  34118  bnj23  34704  kur14lem9  35206  sconnpht  35221  cvmsdisj  35262  sat1el2xp  35371  untelirr  35700  untsucf  35702  dfon2lem4  35779  dfon2lem6  35781  dfon2lem7  35782  dfon2lem8  35783  dfon2  35785  fwddifnp1  36158  domalom  37397  pibt2  37410  poimirlem18  37637  poimirlem21  37640  heibor1lem  37808  heiborlem4  37813  heiborlem6  37815  atlex  39314  psubspi  39746  elpcliN  39892  ldilval  40112  trlord  40568  tendotp  40760  hdmapval2  41831  cantnfresb  43317  pwelg  43553  gneispace0nelrn2  44134  gneispaceel2  44137  gneispacess2  44139  stoweid  46064  iccpartimp  47421  iccpartltu  47429  iccpartgtl  47430  iccpartleu  47432  iccpartgel  47433  isuspgrim0  47898  gricushgr  47921  1arymaptf1  48647