Theorem rspccv 3570

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049

This theorem is referenced by:  elinti  4908  trss  5212  fvn0ssdmfun  7016  dff3  7042  2fvcoidd  7240  ofrval  7631  limsuc  7788  limuni3  7791  peano5  7832  frxp  8065  smo11  8293  odi  8503  supub  9354  suplub  9355  elirrvOLD  9495  dfom3  9548  noinfep  9561  tcrank  9788  alephle  9990  dfac5lem5  10029  dfac2b  10033  cofsmo  10171  coftr  10175  infpssrlem4  10208  isf34lem6  10282  axcc2lem  10338  domtriomlem  10344  axdc2lem  10350  axdc3lem2  10353  axdc4lem  10357  ac5b  10380  zorn2lem2  10399  zorn2lem6  10403  pwcfsdom  10485  inar1  10677  grupw  10697  grupr  10699  gruurn  10700  grothpw  10728  grothpwex  10729  axgroth6  10730  grothomex  10731  nqereu  10831  supsrlem  11013  axpre-sup  11071  dedekind  11287  dedekindle  11288  supmullem1  12103  supmul  12105  peano5nni  12139  dfnn2  12149  peano5uzi  12572  zindd  12584  lcmfdvds  16560  lcmfunsn  16562  1arith  16846  ramcl  16948  clatleglb  18432  pslem  18486  cyccom  19123  rngisomring1  20395  psgndiflemA  21547  eqcoe1ply1eq  22234  mvmumamul1  22489  smadiadetlem0  22596  chpscmat  22777  basis2  22886  tg2  22900  clsndisj  23010  cnpimaex  23191  t1sncld  23261  regsep  23269  nrmsep3  23290  cmpsub  23335  2ndc1stc  23386  refssex  23446  ptfinfin  23454  txcnpi  23543  txcmplem1  23576  tx1stc  23585  filss  23788  ufilss  23840  fclsopni  23950  fclsrest  23959  alexsubb  23981  alexsubALTlem2  23983  alexsubALTlem4  23985  ghmcnp  24050  qustgplem  24056  mopni  24427  metrest  24459  metcnpi  24479  metcnpi2  24480  nmolb  24652  nmoleub2lem2  25063  ovoliunlem1  25450  ovolicc2lem3  25467  mblsplit  25480  fta1b  26124  plycj  26230  plycjOLD  26232  lgamgulmlem1  26986  sqfpc  27094  ostth2lem2  27592  ostth3  27596  sltval2  27615  nogt01o  27655  madebdayim  27853  madebdaylemlrcut  27864  precsexlem9  28173  onsiso  28225  bdayon  28229  dfn0s2  28280  onsfi  28303  peano5uzs  28348  vdiscusgr  29531  0vtxrusgr  29577  rusgrnumwrdl2  29586  ewlkinedg  29604  eupthseg  30207  upgreupthseg  30210  numclwwlk1  30362  l2p  30480  lpni  30481  nvz  30670  chcompl  31243  ocin  31297  hmopidmchi  32152  dmdmd  32301  dmdbr5  32309  mdsl1i  32322  sigaclci  34217  bnj23  34802  kur14lem9  35330  sconnpht  35345  cvmsdisj  35386  sat1el2xp  35495  untelirr  35824  untsucf  35826  dfon2lem4  35900  dfon2lem6  35902  dfon2lem7  35903  dfon2lem8  35904  dfon2  35906  fwddifnp1  36281  domalom  37521  pibt2  37534  poimirlem18  37751  poimirlem21  37754  heibor1lem  37922  heiborlem4  37927  heiborlem6  37929  atlex  39488  psubspi  39919  elpcliN  40065  ldilval  40285  trlord  40741  tendotp  40933  hdmapval2  42004  cantnfresb  43481  pwelg  43717  gneispace0nelrn2  44298  gneispaceel2  44301  gneispacess2  44303  stoweid  46223  iccpartimp  47579  iccpartltu  47587  iccpartgtl  47588  iccpartleu  47590  iccpartgel  47591  isuspgrim0  48056  gricushgr  48079  1arymaptf1  48804