Theorem rspccv 3557

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  elinti  4886  trss  5189  fvn0ssdmfun  7015  dff3  7041  2fvcoidd  7241  ofrval  7632  limsuc  7789  limuni3  7792  peano5  7833  frxp  8066  smo11  8294  odi  8504  supub  9362  suplub  9363  elirrvOLDOLD  9504  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  21576  eqcoe1ply1eq  22285  mvmumamul1  22537  smadiadetlem0  22644  chpscmat  22825  basis2  22934  tg2  22948  clsndisj  23058  cnpimaex  23239  t1sncld  23309  regsep  23317  nrmsep3  23338  cmpsub  23383  2ndc1stc  23434  refssex  23494  ptfinfin  23502  txcnpi  23591  txcmplem1  23624  tx1stc  23633  filss  23836  ufilss  23888  fclsopni  23998  fclsrest  24007  alexsubb  24029  alexsubALTlem2  24031  alexsubALTlem4  24033  ghmcnp  24098  qustgplem  24104  mopni  24475  metrest  24507  metcnpi  24527  metcnpi2  24528  nmolb  24700  nmoleub2lem2  25101  ovoliunlem1  25487  ovolicc2lem3  25504  mblsplit  25517  fta1b  26155  plycj  26260  plycjOLD  26262  lgamgulmlem1  27010  sqfpc  27118  ostth2lem2  27615  ostth3  27619  ltsval2  27638  nogt01o  27678  madebdayim  27898  madebdaylemlrcut  27909  precsexlem9  28225  oniso  28281  bdayons  28286  dfn0s2  28342  onsfi  28366  peano5uzs  28414  bdaypw2n0bndlem  28473  vdiscusgr  29618  0vtxrusgr  29664  rusgrnumwrdl2  29673  ewlkinedg  29691  eupthseg  30294  upgreupthseg  30297  numclwwlk1  30449  l2p  30568  lpni  30569  nvz  30758  chcompl  31331  ocin  31385  hmopidmchi  32240  dmdmd  32389  dmdbr5  32397  mdsl1i  32410  sigaclci  34316  bnj23  34901  kur14lem9  35442  sconnpht  35457  cvmsdisj  35498  sat1el2xp  35607  untelirr  35936  untsucf  35938  dfon2lem4  36012  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  fwddifnp1  36393  domalom  37766  pibt2  37779  poimirlem18  38005  poimirlem21  38008  heibor1lem  38176  heiborlem4  38181  heiborlem6  38183  atlex  39808  psubspi  40239  elpcliN  40385  ldilval  40605  trlord  41061  tendotp  41253  hdmapval2  42324  cantnfresb  43769  pwelg  44004  gneispace0nelrn2  44585  gneispaceel2  44588  gneispacess2  44590  stoweid  46506  iccpartimp  47892  iccpartltu  47900  iccpartgtl  47901  iccpartleu  47903  iccpartgel  47904  isuspgrim0  48385  gricushgr  48408  1arymaptf1  49133