Theorem rspccv 3588

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3045

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  elinti  4922  trss  5228  fvn0ssdmfun  7049  dff3  7075  2fvcoidd  7275  ofrval  7668  limsuc  7828  limuni3  7831  peano5  7872  frxp  8108  smo11  8336  odi  8546  supub  9417  suplub  9418  elirrv  9556  dfom3  9607  noinfep  9620  tcrank  9844  alephle  10048  dfac5lem5  10087  dfac2b  10091  cofsmo  10229  coftr  10233  infpssrlem4  10266  isf34lem6  10340  axcc2lem  10396  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  axdc4lem  10415  ac5b  10438  zorn2lem2  10457  zorn2lem6  10461  pwcfsdom  10543  inar1  10735  grupw  10755  grupr  10757  gruurn  10758  grothpw  10786  grothpwex  10787  axgroth6  10788  grothomex  10789  nqereu  10889  supsrlem  11071  axpre-sup  11129  dedekind  11344  dedekindle  11345  supmullem1  12160  supmul  12162  peano5nni  12196  dfnn2  12206  peano5uzi  12630  zindd  12642  lcmfdvds  16619  lcmfunsn  16621  1arith  16905  ramcl  17007  clatleglb  18484  pslem  18538  cyccom  19142  rngisomring1  20384  psgndiflemA  21517  eqcoe1ply1eq  22193  mvmumamul1  22448  smadiadetlem0  22555  chpscmat  22736  basis2  22845  tg2  22859  clsndisj  22969  cnpimaex  23150  t1sncld  23220  regsep  23228  nrmsep3  23249  cmpsub  23294  2ndc1stc  23345  refssex  23405  ptfinfin  23413  txcnpi  23502  txcmplem1  23535  tx1stc  23544  filss  23747  ufilss  23799  fclsopni  23909  fclsrest  23918  alexsubb  23940  alexsubALTlem2  23942  alexsubALTlem4  23944  ghmcnp  24009  qustgplem  24015  mopni  24387  metrest  24419  metcnpi  24439  metcnpi2  24440  nmolb  24612  nmoleub2lem2  25023  ovoliunlem1  25410  ovolicc2lem3  25427  mblsplit  25440  fta1b  26084  plycj  26190  plycjOLD  26192  lgamgulmlem1  26946  sqfpc  27054  ostth2lem2  27552  ostth3  27556  sltval2  27575  nogt01o  27615  madebdayim  27806  madebdaylemlrcut  27817  precsexlem9  28124  onsiso  28176  bdayon  28180  dfn0s2  28231  onsfi  28254  peano5uzs  28299  vdiscusgr  29466  0vtxrusgr  29512  rusgrnumwrdl2  29521  ewlkinedg  29539  eupthseg  30142  upgreupthseg  30145  numclwwlk1  30297  l2p  30415  lpni  30416  nvz  30605  chcompl  31178  ocin  31232  hmopidmchi  32087  dmdmd  32236  dmdbr5  32244  mdsl1i  32257  sigaclci  34129  bnj23  34715  kur14lem9  35208  sconnpht  35223  cvmsdisj  35264  sat1el2xp  35373  untelirr  35702  untsucf  35704  dfon2lem4  35781  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon2  35787  fwddifnp1  36160  domalom  37399  pibt2  37412  poimirlem18  37639  poimirlem21  37642  heibor1lem  37810  heiborlem4  37815  heiborlem6  37817  atlex  39316  psubspi  39748  elpcliN  39894  ldilval  40114  trlord  40570  tendotp  40762  hdmapval2  41833  cantnfresb  43320  pwelg  43556  gneispace0nelrn2  44137  gneispaceel2  44140  gneispacess2  44142  stoweid  46068  iccpartimp  47422  iccpartltu  47430  iccpartgtl  47431  iccpartleu  47433  iccpartgel  47434  isuspgrim0  47898  gricushgr  47921  1arymaptf1  48635