Theorem rspccv 3577

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076

This theorem is referenced by:  elinti  4911  trss  5214  fvn0ssdmfun  7050  dff3  7076  2fvcoidd  7276  ofrval  7667  limsuc  7824  limuni3  7827  peano5  7869  frxp  8100  smo11  8329  odi  8542  supub  9399  suplub  9400  elirrvOLDOLD  9541  dfom3  9596  noinfep  9609  tcrank  9836  alephle  10038  dfac5lem5  10077  dfac2b  10081  cofsmo  10220  coftr  10224  infpssrlem4  10257  isf34lem6  10331  axcc2lem  10387  domtriomlem  10393  axdc2lem  10399  axdc3lem2  10402  axdc4lem  10406  ac5b  10429  zorn2lem2  10448  zorn2lem6  10452  pwcfsdom  10535  inar1  10727  grupw  10747  grupr  10749  gruurn  10750  grothpw  10778  grothpwex  10779  axgroth6  10780  grothomex  10781  nqereu  10881  supsrlem  11063  axpre-sup  11121  dedekind  11340  dedekindle  11341  supmullem1  12156  supmul  12158  peano5nni  12207  dfnn2  12217  peano5uzi  12656  zindd  12668  lcmfdvds  16667  lcmfunsn  16669  1arith  16954  ramcl  17056  clatleglb  18541  pslem  18595  cyccom  19235  rngisomring1  20504  psgndiflemA  21641  eqcoe1ply1eq  22350  mvmumamul1  22602  smadiadetlem0  22709  chpscmat  22890  basis2  22999  tg2  23013  clsndisj  23123  cnpimaex  23304  t1sncld  23374  regsep  23382  nrmsep3  23403  cmpsub  23448  2ndc1stc  23499  refssex  23559  ptfinfin  23567  txcnpi  23656  txcmplem1  23689  tx1stc  23698  filss  23901  ufilss  23953  fclsopni  24063  fclsrest  24072  alexsubb  24094  alexsubALTlem2  24096  alexsubALTlem4  24098  ghmcnp  24163  qustgplem  24169  mopni  24540  metrest  24572  metcnpi  24592  metcnpi2  24593  nmolb  24765  nmoleub2lem2  25166  ovoliunlem1  25552  ovolicc2lem3  25569  mblsplit  25582  fta1b  26220  plycj  26325  plycjOLD  26327  lgamgulmlem1  27081  sqfpc  27189  ostth2lem2  27686  ostth3  27690  ltsval2  27708  nogt01o  27748  madebdayim  27969  madebdaylemlrcut  27980  precsexlem9  28296  oniso  28352  bdayons  28357  dfn0s2  28413  onsfi  28437  peano5uzs  28485  bdaypw2n0bndlem  28544  vdiscusgr  29689  0vtxrusgr  29735  rusgrnumwrdl2  29744  ewlkinedg  29762  eupthseg  30365  upgreupthseg  30368  numclwwlk1  30520  l2p  30639  lpni  30640  nvz  30829  chcompl  31402  ocin  31456  hmopidmchi  32311  dmdmd  32460  dmdbr5  32468  mdsl1i  32481  sigaclci  34390  bnj23  34975  kur14lem9  35525  sconnpht  35540  cvmsdisj  35581  sat1el2xp  35690  untelirr  36019  untsucf  36021  dfon2lem4  36095  dfon2lem6  36097  dfon2lem7  36098  dfon2lem8  36099  dfon2  36101  fwddifnp1  36476  domalom  37859  pibt2  37872  poimirlem18  38098  poimirlem21  38101  heibor1lem  38269  heiborlem4  38274  heiborlem6  38276  atlex  39901  psubspi  40332  elpcliN  40478  ldilval  40698  trlord  41154  tendotp  41346  hdmapval2  42417  cantnfresb  43862  pwelg  44097  gneispace0nelrn2  44678  gneispaceel2  44681  gneispacess2  44683  stoweid  46598  iccpartimp  47984  iccpartltu  47992  iccpartgtl  47993  iccpartleu  47995  iccpartgel  47996  isuspgrim0  48477  gricushgr  48500  1arymaptf1  49225