Theorem rspccv 3562

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  elinti  4899  trss  5203  fvn0ssdmfun  7020  dff3  7046  2fvcoidd  7245  ofrval  7636  limsuc  7793  limuni3  7796  peano5  7837  frxp  8069  smo11  8297  odi  8507  supub  9365  suplub  9366  elirrvOLD  9506  dfom3  9559  noinfep  9572  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  10497  inar1  10689  grupw  10709  grupr  10711  gruurn  10712  grothpw  10740  grothpwex  10741  axgroth6  10742  grothomex  10743  nqereu  10843  supsrlem  11025  axpre-sup  11083  dedekind  11300  dedekindle  11301  supmullem1  12117  supmul  12119  peano5nni  12168  dfnn2  12178  peano5uzi  12609  zindd  12621  lcmfdvds  16602  lcmfunsn  16604  1arith  16889  ramcl  16991  clatleglb  18475  pslem  18529  cyccom  19169  rngisomring1  20439  psgndiflemA  21591  eqcoe1ply1eq  22274  mvmumamul1  22529  smadiadetlem0  22636  chpscmat  22817  basis2  22926  tg2  22940  clsndisj  23050  cnpimaex  23231  t1sncld  23301  regsep  23309  nrmsep3  23330  cmpsub  23375  2ndc1stc  23426  refssex  23486  ptfinfin  23494  txcnpi  23583  txcmplem1  23616  tx1stc  23625  filss  23828  ufilss  23880  fclsopni  23990  fclsrest  23999  alexsubb  24021  alexsubALTlem2  24023  alexsubALTlem4  24025  ghmcnp  24090  qustgplem  24096  mopni  24467  metrest  24499  metcnpi  24519  metcnpi2  24520  nmolb  24692  nmoleub2lem2  25093  ovoliunlem1  25479  ovolicc2lem3  25496  mblsplit  25509  fta1b  26147  plycj  26252  plycjOLD  26254  lgamgulmlem1  27006  sqfpc  27114  ostth2lem2  27611  ostth3  27615  ltsval2  27634  nogt01o  27674  madebdayim  27894  madebdaylemlrcut  27905  precsexlem9  28221  oniso  28277  bdayons  28282  dfn0s2  28338  onsfi  28362  peano5uzs  28410  bdaypw2n0bndlem  28469  vdiscusgr  29615  0vtxrusgr  29661  rusgrnumwrdl2  29670  ewlkinedg  29688  eupthseg  30291  upgreupthseg  30294  numclwwlk1  30446  l2p  30565  lpni  30566  nvz  30755  chcompl  31328  ocin  31382  hmopidmchi  32237  dmdmd  32386  dmdbr5  32394  mdsl1i  32407  sigaclci  34292  bnj23  34877  kur14lem9  35412  sconnpht  35427  cvmsdisj  35468  sat1el2xp  35577  untelirr  35906  untsucf  35908  dfon2lem4  35982  dfon2lem6  35984  dfon2lem7  35985  dfon2lem8  35986  dfon2  35988  fwddifnp1  36363  domalom  37734  pibt2  37747  poimirlem18  37973  poimirlem21  37976  heibor1lem  38144  heiborlem4  38149  heiborlem6  38151  atlex  39776  psubspi  40207  elpcliN  40353  ldilval  40573  trlord  41029  tendotp  41221  hdmapval2  42292  cantnfresb  43770  pwelg  44005  gneispace0nelrn2  44586  gneispaceel2  44589  gneispacess2  44591  stoweid  46509  iccpartimp  47889  iccpartltu  47897  iccpartgtl  47898  iccpartleu  47900  iccpartgel  47901  isuspgrim0  48382  gricushgr  48405  1arymaptf1  49130