Theorem rspccv 3610

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

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

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  elinti  4960  trss  5277  fvn0ssdmfun  7077  dff3  7102  2fvcoidd  7295  ofrval  7682  limsuc  7838  limuni3  7841  peano5  7884  frxp  8112  wfrdmclOLD  8317  smo11  8364  odi  8579  supub  9454  suplub  9455  elirrv  9591  dfom3  9642  noinfep  9655  tcrank  9879  alephle  10083  dfac5lem5  10122  dfac2b  10125  cofsmo  10264  coftr  10268  infpssrlem4  10301  isf34lem6  10375  axcc2lem  10431  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc4lem  10450  ac5b  10473  zorn2lem2  10492  zorn2lem6  10496  pwcfsdom  10578  inar1  10770  grupw  10790  grupr  10792  gruurn  10793  grothpw  10821  grothpwex  10822  axgroth6  10823  grothomex  10824  nqereu  10924  supsrlem  11106  axpre-sup  11164  dedekind  11377  dedekindle  11378  supmullem1  12184  supmul  12186  peano5nni  12215  dfnn2  12225  peano5uzi  12651  zindd  12663  lcmfdvds  16579  lcmfunsn  16581  1arith  16860  ramcl  16962  clatleglb  18471  pslem  18525  cyccom  19080  psgndiflemA  21154  eqcoe1ply1eq  21821  mvmumamul1  22056  smadiadetlem0  22163  chpscmat  22344  basis2  22454  tg2  22468  clsndisj  22579  cnpimaex  22760  t1sncld  22830  regsep  22838  nrmsep3  22859  cmpsub  22904  2ndc1stc  22955  refssex  23015  ptfinfin  23023  txcnpi  23112  txcmplem1  23145  tx1stc  23154  filss  23357  ufilss  23409  fclsopni  23519  fclsrest  23528  alexsubb  23550  alexsubALTlem2  23552  alexsubALTlem4  23554  ghmcnp  23619  qustgplem  23625  mopni  24001  metrest  24033  metcnpi  24053  metcnpi2  24054  nmolb  24234  nmoleub2lem2  24632  ovoliunlem1  25019  ovolicc2lem3  25036  mblsplit  25049  fta1b  25687  plycj  25791  lgamgulmlem1  26533  sqfpc  26641  ostth2lem2  27137  ostth3  27141  sltval2  27159  nogt01o  27199  madebdayim  27382  madebdaylemlrcut  27393  precsexlem9  27661  vdiscusgr  28788  0vtxrusgr  28834  rusgrnumwrdl2  28843  ewlkinedg  28861  eupthseg  29459  upgreupthseg  29462  numclwwlk1  29614  l2p  29732  lpni  29733  nvz  29922  chcompl  30495  ocin  30549  hmopidmchi  31404  dmdmd  31553  dmdbr5  31561  mdsl1i  31574  sigaclci  33130  bnj23  33729  kur14lem9  34205  sconnpht  34220  cvmsdisj  34261  sat1el2xp  34370  untelirr  34677  untsucf  34679  dfon2lem4  34758  dfon2lem6  34760  dfon2lem7  34761  dfon2lem8  34762  dfon2  34764  fwddifnp1  35137  domalom  36285  pibt2  36298  poimirlem18  36506  poimirlem21  36509  heibor1lem  36677  heiborlem4  36682  heiborlem6  36684  atlex  38186  psubspi  38618  elpcliN  38764  ldilval  38984  trlord  39440  tendotp  39632  hdmapval2  40703  cantnfresb  42074  pwelg  42311  gneispace0nelrn2  42892  gneispaceel2  42895  gneispacess2  42897  stoweid  44779  iccpartimp  46085  iccpartltu  46093  iccpartgtl  46094  iccpartleu  46096  iccpartgel  46097  isomushgr  46494  isomuspgrlem1  46495  isomuspgr  46502  isomgrtrlem  46506  rngisomring1  46720  1arymaptf1  47328