Theorem rspccv 3559

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  elinti  4889  trss  5201  fvn0ssdmfun  6961  dff3  6985  2fvcoidd  7178  ofrval  7554  limsuc  7705  limuni3  7708  peano5  7749  frxp  7976  wfrdmclOLD  8157  smo11  8204  odi  8419  supub  9227  suplub  9228  elirrv  9364  dfom3  9414  noinfep  9427  tcrank  9651  alephle  9853  dfac5lem5  9892  dfac2b  9895  cofsmo  10034  coftr  10038  infpssrlem4  10071  isf34lem6  10145  axcc2lem  10201  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  axdc4lem  10220  ac5b  10243  zorn2lem2  10262  zorn2lem6  10266  pwcfsdom  10348  inar1  10540  grupw  10560  grupr  10562  gruurn  10563  grothpw  10591  grothpwex  10592  axgroth6  10593  grothomex  10594  nqereu  10694  supsrlem  10876  axpre-sup  10934  dedekind  11147  dedekindle  11148  supmullem1  11954  supmul  11956  peano5nni  11985  dfnn2  11995  peano5uzi  12418  zindd  12430  lcmfdvds  16356  lcmfunsn  16358  1arith  16637  ramcl  16739  clatleglb  18245  pslem  18299  cyccom  18831  cygablOLD  19501  psgndiflemA  20815  eqcoe1ply1eq  21477  mvmumamul1  21712  smadiadetlem0  21819  chpscmat  22000  basis2  22110  tg2  22124  clsndisj  22235  cnpimaex  22416  t1sncld  22486  regsep  22494  nrmsep3  22515  cmpsub  22560  2ndc1stc  22611  refssex  22671  ptfinfin  22679  txcnpi  22768  txcmplem1  22801  tx1stc  22810  filss  23013  ufilss  23065  fclsopni  23175  fclsrest  23184  alexsubb  23206  alexsubALTlem2  23208  alexsubALTlem4  23210  ghmcnp  23275  qustgplem  23281  mopni  23657  metrest  23689  metcnpi  23709  metcnpi2  23710  nmolb  23890  nmoleub2lem2  24288  ovoliunlem1  24675  ovolicc2lem3  24692  mblsplit  24705  fta1b  25343  plycj  25447  lgamgulmlem1  26187  sqfpc  26295  ostth2lem2  26791  ostth3  26795  vdiscusgr  27907  0vtxrusgr  27953  rusgrnumwrdl2  27962  ewlkinedg  27980  eupthseg  28579  upgreupthseg  28582  numclwwlk1  28734  l2p  28850  lpni  28851  nvz  29040  chcompl  29613  ocin  29667  hmopidmchi  30522  dmdmd  30671  dmdbr5  30679  mdsl1i  30692  sigaclci  32109  bnj23  32706  kur14lem9  33185  sconnpht  33200  cvmsdisj  33241  sat1el2xp  33350  untelirr  33658  untsucf  33660  dfon2lem4  33771  dfon2lem6  33773  dfon2lem7  33774  dfon2lem8  33775  dfon2  33777  sltval2  33868  nogt01o  33908  madebdayim  34079  madebdaylemlrcut  34088  fwddifnp1  34476  domalom  35584  pibt2  35597  poimirlem18  35804  poimirlem21  35807  heibor1lem  35976  heiborlem4  35981  heiborlem6  35983  atlex  37337  psubspi  37768  elpcliN  37914  ldilval  38134  trlord  38590  tendotp  38782  hdmapval2  39853  pwelg  41174  gneispace0nelrn2  41758  gneispaceel2  41761  gneispacess2  41763  stoweid  43611  iccpartimp  44880  iccpartltu  44888  iccpartgtl  44889  iccpartleu  44891  iccpartgel  44892  isomushgr  45289  isomuspgrlem1  45290  isomuspgr  45297  isomgrtrlem  45301  1arymaptf1  45999