Theorem rspccv 3582

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 3581	. 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  4915  trss  5220  fvn0ssdmfun  7028  dff3  7054  2fvcoidd  7254  ofrval  7645  limsuc  7805  limuni3  7808  peano5  7849  frxp  8082  smo11  8310  odi  8520  supub  9386  suplub  9387  elirrv  9525  dfom3  9576  noinfep  9589  tcrank  9813  alephle  10017  dfac5lem5  10056  dfac2b  10060  cofsmo  10198  coftr  10202  infpssrlem4  10235  isf34lem6  10309  axcc2lem  10365  domtriomlem  10371  axdc2lem  10377  axdc3lem2  10380  axdc4lem  10384  ac5b  10407  zorn2lem2  10426  zorn2lem6  10430  pwcfsdom  10512  inar1  10704  grupw  10724  grupr  10726  gruurn  10727  grothpw  10755  grothpwex  10756  axgroth6  10757  grothomex  10758  nqereu  10858  supsrlem  11040  axpre-sup  11098  dedekind  11313  dedekindle  11314  supmullem1  12129  supmul  12131  peano5nni  12165  dfnn2  12175  peano5uzi  12599  zindd  12611  lcmfdvds  16588  lcmfunsn  16590  1arith  16874  ramcl  16976  clatleglb  18453  pslem  18507  cyccom  19111  rngisomring1  20353  psgndiflemA  21486  eqcoe1ply1eq  22162  mvmumamul1  22417  smadiadetlem0  22524  chpscmat  22705  basis2  22814  tg2  22828  clsndisj  22938  cnpimaex  23119  t1sncld  23189  regsep  23197  nrmsep3  23218  cmpsub  23263  2ndc1stc  23314  refssex  23374  ptfinfin  23382  txcnpi  23471  txcmplem1  23504  tx1stc  23513  filss  23716  ufilss  23768  fclsopni  23878  fclsrest  23887  alexsubb  23909  alexsubALTlem2  23911  alexsubALTlem4  23913  ghmcnp  23978  qustgplem  23984  mopni  24356  metrest  24388  metcnpi  24408  metcnpi2  24409  nmolb  24581  nmoleub2lem2  24992  ovoliunlem1  25379  ovolicc2lem3  25396  mblsplit  25409  fta1b  26053  plycj  26159  plycjOLD  26161  lgamgulmlem1  26915  sqfpc  27023  ostth2lem2  27521  ostth3  27525  sltval2  27544  nogt01o  27584  madebdayim  27775  madebdaylemlrcut  27786  precsexlem9  28093  onsiso  28145  bdayon  28149  dfn0s2  28200  onsfi  28223  peano5uzs  28268  vdiscusgr  29435  0vtxrusgr  29481  rusgrnumwrdl2  29490  ewlkinedg  29508  eupthseg  30108  upgreupthseg  30111  numclwwlk1  30263  l2p  30381  lpni  30382  nvz  30571  chcompl  31144  ocin  31198  hmopidmchi  32053  dmdmd  32202  dmdbr5  32210  mdsl1i  32223  sigaclci  34095  bnj23  34681  kur14lem9  35174  sconnpht  35189  cvmsdisj  35230  sat1el2xp  35339  untelirr  35668  untsucf  35670  dfon2lem4  35747  dfon2lem6  35749  dfon2lem7  35750  dfon2lem8  35751  dfon2  35753  fwddifnp1  36126  domalom  37365  pibt2  37378  poimirlem18  37605  poimirlem21  37608  heibor1lem  37776  heiborlem4  37781  heiborlem6  37783  atlex  39282  psubspi  39714  elpcliN  39860  ldilval  40080  trlord  40536  tendotp  40728  hdmapval2  41799  cantnfresb  43286  pwelg  43522  gneispace0nelrn2  44103  gneispaceel2  44106  gneispacess2  44108  stoweid  46034  iccpartimp  47391  iccpartltu  47399  iccpartgtl  47400  iccpartleu  47402  iccpartgel  47403  isuspgrim0  47867  gricushgr  47890  1arymaptf1  48604