Theorem rspccv 3568

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  elinti  4847  trss  5145  fvn0ssdmfun  6819  dff3  6843  2fvcoidd  7031  ofrval  7399  limsuc  7544  limuni3  7547  frxp  7803  wfrdmcl  7946  smo11  7984  odi  8188  supub  8907  suplub  8908  elirrv  9044  dfom3  9094  noinfep  9107  tcrank  9297  alephle  9499  dfac5lem5  9538  dfac2b  9541  cofsmo  9680  coftr  9684  infpssrlem4  9717  isf34lem6  9791  axcc2lem  9847  domtriomlem  9853  axdc2lem  9859  axdc3lem2  9862  axdc4lem  9866  ac5b  9889  zorn2lem2  9908  zorn2lem6  9912  pwcfsdom  9994  inar1  10186  grupw  10206  grupr  10208  gruurn  10209  grothpw  10237  grothpwex  10238  axgroth6  10239  grothomex  10240  nqereu  10340  supsrlem  10522  axpre-sup  10580  dedekind  10792  dedekindle  10793  supmullem1  11598  supmul  11600  peano5nni  11628  dfnn2  11638  peano5uzi  12059  zindd  12071  lcmfdvds  15976  lcmfunsn  15978  1arith  16253  ramcl  16355  clatleglb  17728  pslem  17808  cyccom  18338  cygablOLD  19004  psgndiflemA  20290  eqcoe1ply1eq  20926  mvmumamul1  21159  smadiadetlem0  21266  chpscmat  21447  basis2  21556  tg2  21570  clsndisj  21680  cnpimaex  21861  t1sncld  21931  regsep  21939  nrmsep3  21960  cmpsub  22005  2ndc1stc  22056  refssex  22116  ptfinfin  22124  txcnpi  22213  txcmplem1  22246  tx1stc  22255  filss  22458  ufilss  22510  fclsopni  22620  fclsrest  22629  alexsubb  22651  alexsubALTlem2  22653  alexsubALTlem4  22655  ghmcnp  22720  qustgplem  22726  mopni  23099  metrest  23131  metcnpi  23151  metcnpi2  23152  nmolb  23323  nmoleub2lem2  23721  ovoliunlem1  24106  ovolicc2lem3  24123  mblsplit  24136  fta1b  24770  plycj  24874  lgamgulmlem1  25614  sqfpc  25722  ostth2lem2  26218  ostth3  26222  vdiscusgr  27321  0vtxrusgr  27367  rusgrnumwrdl2  27376  ewlkinedg  27394  eupthseg  27991  upgreupthseg  27994  numclwwlk1  28146  l2p  28262  lpni  28263  nvz  28452  chcompl  29025  ocin  29079  hmopidmchi  29934  dmdmd  30083  dmdbr5  30091  mdsl1i  30104  sigaclci  31501  bnj23  32098  kur14lem9  32574  sconnpht  32589  cvmsdisj  32630  sat1el2xp  32739  untelirr  33047  untsucf  33049  dfon2lem4  33144  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon2  33150  sltval2  33276  fwddifnp1  33739  domalom  34821  pibt2  34834  poimirlem18  35075  poimirlem21  35078  heibor1lem  35247  heiborlem4  35252  heiborlem6  35254  atlex  36612  psubspi  37043  elpcliN  37189  ldilval  37409  trlord  37865  tendotp  38057  hdmapval2  39128  pwelg  40259  gneispace0nelrn2  40844  gneispaceel2  40847  gneispacess2  40849  stoweid  42705  iccpartimp  43934  iccpartltu  43942  iccpartgtl  43943  iccpartleu  43945  iccpartgel  43946  isomushgr  44344  isomuspgrlem1  44345  isomuspgr  44352  isomgrtrlem  44356  1arymaptf1  45056