Theorem rspccv 3585

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 3584	. 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  4919  trss  5225  fvn0ssdmfun  7046  dff3  7072  2fvcoidd  7272  ofrval  7665  limsuc  7825  limuni3  7828  peano5  7869  frxp  8105  smo11  8333  odi  8543  supub  9410  suplub  9411  elirrv  9549  dfom3  9600  noinfep  9613  tcrank  9837  alephle  10041  dfac5lem5  10080  dfac2b  10084  cofsmo  10222  coftr  10226  infpssrlem4  10259  isf34lem6  10333  axcc2lem  10389  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  axdc4lem  10408  ac5b  10431  zorn2lem2  10450  zorn2lem6  10454  pwcfsdom  10536  inar1  10728  grupw  10748  grupr  10750  gruurn  10751  grothpw  10779  grothpwex  10780  axgroth6  10781  grothomex  10782  nqereu  10882  supsrlem  11064  axpre-sup  11122  dedekind  11337  dedekindle  11338  supmullem1  12153  supmul  12155  peano5nni  12189  dfnn2  12199  peano5uzi  12623  zindd  12635  lcmfdvds  16612  lcmfunsn  16614  1arith  16898  ramcl  17000  clatleglb  18477  pslem  18531  cyccom  19135  rngisomring1  20377  psgndiflemA  21510  eqcoe1ply1eq  22186  mvmumamul1  22441  smadiadetlem0  22548  chpscmat  22729  basis2  22838  tg2  22852  clsndisj  22962  cnpimaex  23143  t1sncld  23213  regsep  23221  nrmsep3  23242  cmpsub  23287  2ndc1stc  23338  refssex  23398  ptfinfin  23406  txcnpi  23495  txcmplem1  23528  tx1stc  23537  filss  23740  ufilss  23792  fclsopni  23902  fclsrest  23911  alexsubb  23933  alexsubALTlem2  23935  alexsubALTlem4  23937  ghmcnp  24002  qustgplem  24008  mopni  24380  metrest  24412  metcnpi  24432  metcnpi2  24433  nmolb  24605  nmoleub2lem2  25016  ovoliunlem1  25403  ovolicc2lem3  25420  mblsplit  25433  fta1b  26077  plycj  26183  plycjOLD  26185  lgamgulmlem1  26939  sqfpc  27047  ostth2lem2  27545  ostth3  27549  sltval2  27568  nogt01o  27608  madebdayim  27799  madebdaylemlrcut  27810  precsexlem9  28117  onsiso  28169  bdayon  28173  dfn0s2  28224  onsfi  28247  peano5uzs  28292  vdiscusgr  29459  0vtxrusgr  29505  rusgrnumwrdl2  29514  ewlkinedg  29532  eupthseg  30135  upgreupthseg  30138  numclwwlk1  30290  l2p  30408  lpni  30409  nvz  30598  chcompl  31171  ocin  31225  hmopidmchi  32080  dmdmd  32229  dmdbr5  32237  mdsl1i  32250  sigaclci  34122  bnj23  34708  kur14lem9  35201  sconnpht  35216  cvmsdisj  35257  sat1el2xp  35366  untelirr  35695  untsucf  35697  dfon2lem4  35774  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon2  35780  fwddifnp1  36153  domalom  37392  pibt2  37405  poimirlem18  37632  poimirlem21  37635  heibor1lem  37803  heiborlem4  37808  heiborlem6  37810  atlex  39309  psubspi  39741  elpcliN  39887  ldilval  40107  trlord  40563  tendotp  40755  hdmapval2  41826  cantnfresb  43313  pwelg  43549  gneispace0nelrn2  44130  gneispaceel2  44133  gneispacess2  44135  stoweid  46061  iccpartimp  47418  iccpartltu  47426  iccpartgtl  47427  iccpartleu  47429  iccpartgel  47430  isuspgrim0  47894  gricushgr  47917  1arymaptf1  48631