Theorem rspccv 3578

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  elinti  4921  trss  5228  fvn0ssdmfun  7069  dff3  7095  2fvcoidd  7295  ofrval  7686  limsuc  7841  limuni3  7844  peano5  7886  frxp  8118  smo11  8347  odi  8560  supub  9415  suplub  9416  elirrvOLDOLD  9557  dfom3  9612  noinfep  9625  tcrank  9852  alephle  10068  dfac5lem5  10107  dfac2b  10110  cofsmo  10248  coftr  10252  infpssrlem4  10285  isf34lem6  10359  axcc2lem  10415  domtriomlem  10421  axdc2lem  10427  axdc3lem2  10430  axdc4lem  10434  ac5b  10457  zorn2lem2  10476  zorn2lem6  10480  pwcfsdom  10563  inar1  10755  grupw  10775  grupr  10777  gruurn  10778  grothpw  10806  grothpwex  10807  axgroth6  10808  grothomex  10809  nqereu  10909  supsrlem  11091  axpre-sup  11149  dedekind  11368  dedekindle  11369  supmullem1  12180  supmul  12182  peano5nni  12231  dfnn2  12241  peano5uzi  12680  zindd  12692  lcmfdvds  16695  lcmfunsn  16697  1arith  16982  ramcl  17084  clatleglb  18569  pslem  18623  cyccom  19269  rngisomring1  20546  isdrng3lem2  20852  psgndiflemA  21751  eqcoe1ply1eq  22459  mvmumamul1  22711  smadiadetlem0  22818  chpscmat  22999  basis2  23108  tg2  23122  clsndisj  23232  cnpimaex  23413  t1sncld  23483  regsep  23491  nrmsep3  23512  cmpsub  23557  2ndc1stc  23608  refssex  23668  ptfinfin  23676  txcnpi  23765  txcmplem1  23798  tx1stc  23807  filss  24010  ufilss  24062  fclsopni  24172  fclsrest  24181  alexsubb  24203  alexsubALTlem2  24205  alexsubALTlem4  24207  ghmcnp  24272  qustgplem  24278  mopni  24649  metrest  24681  metcnpi  24701  metcnpi2  24702  nmolb  24874  nmoleub2lem2  25275  ovoliunlem1  25661  ovolicc2lem3  25678  mblsplit  25691  fta1b  26329  plycj  26434  plycjOLD  26436  lgamgulmlem1  27193  sqfpc  27301  ostth2lem2  27798  ostth3  27802  ltsval2  27820  nogt01o  27860  madebdayim  28081  madebdaylemlrcut  28092  precsexlem9  28408  oniso  28464  bdayons  28469  dfn0s2  28525  onsfi  28549  peano5uzs  28597  bdaypw2n0bndlem  28656  vdiscusgr  29881  0vtxrusgr  29927  rusgrnumwrdl2  29936  ewlkinedg  29954  eupthseg  30557  upgreupthseg  30560  numclwwlk1  30712  l2p  30831  lpni  30832  nvz  31021  chcompl  31594  ocin  31648  hmopidmchi  32503  dmdmd  32652  dmdbr5  32660  mdsl1i  32673  sigaclci  34522  bnj23  35107  kur14lem9  35706  sconnpht  35721  cvmsdisj  35762  sat1el2xp  35871  untelirr  36200  untsucf  36202  dfon2lem4  36276  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  fwddifnp1  36657  domalom  38050  pibt2  38063  poimirlem18  38289  poimirlem21  38292  heibor1lem  38460  heiborlem4  38465  heiborlem6  38467  atlex  40090  psubspi  40521  elpcliN  40667  ldilval  40887  trlord  41343  tendotp  41535  hdmapval2  42606  cantnfresb  44051  pwelg  44286  gneispace0nelrn2  44867  gneispaceel2  44870  gneispacess2  44872  stoweid  46777  iccpartimp  48166  iccpartltu  48174  iccpartgtl  48175  iccpartleu  48177  iccpartgel  48178  isuspgrim0  48659  gricushgr  48682  1arymaptf1  49422