Theorem rspcva 3558

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcva	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3556	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  rexraleqim  3585  fsneq  6976  fvn0ssdmfun  7015  fveqdmss  7019  fvcofneq  7034  wfr3g  8259  boxriin  8878  boxcutc  8879  pwssfi  9101  marypha1lem  9336  supmo  9355  infmo  9400  unwdomg  9489  frr3g  9671  isinffi  9907  axdc3lem2  10364  grothac  10744  nqereu  10843  nnsub  12212  zextle  12593  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  injresinjlem  13736  ssnn0fi  13938  suppssfz  13947  faclbnd4lem4  14249  ishashinf  14416  rexuz3  15302  cau3lem  15308  caubnd2  15311  o1co  15539  climcn1  15545  incexclem  15792  dvdsext  16281  mreintcl  17548  initoeu1  17969  initoeu2  17974  termoeu1  17976  lublecllem  18315  mgmidmo  18619  gsumval2  18645  dfgrp3lem  19005  symgfix2  19382  odeq  19516  gexid  19547  ringurd  20157  o2timesd  20182  rglcom4d  20183  gsummoncoe1  22294  m2detleiblem3  22612  m2detleiblem4  22613  cpmatmcllem  22701  mp2pm2mplem4  22792  cayleyhamilton1  22875  cmpsublem  23382  cmpsub  23383  cmpfii  23392  ptpjcn  23594  isufil2  23891  ufileu  23902  lmmbr  25243  caussi  25282  plyco0  26175  dgrco  26258  emcllem7  26983  isppw2  27096  addsrid  27974  mulsrid  28123  n0subs  28373  uvtxnbgrvtx  29480  rusgrnumwwlks  30063  clwwlkf  30135  vdgn1frgrv2  30384  frgrregorufr  30413  grpoidinvlem3  30595  grpoideu  30598  lnconi  32122  fsumiunle  32921  tpr2rico  34096  esumiun  34278  0elsiga  34298  sigaclci  34316  dya2icoseg2  34462  derangsn  35398  sat1el2xp  35607  fwddifnp1  36393  poimirlem25  38012  poimirlem26  38013  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  heicant  38022  mblfinlem2  38025  ftc1anc  38068  fdc  38112  bndss  38153  isdrngo2  38325  divrngidl  38395  maxidlmax  38410  cdleme0nex  40782  dihglblem2N  41786  hgmapvs  42383  ismrcd1  43147  nacsfg  43154  isnacs3  43159  nacsfix  43161  mzpcl1  43178  mzpcl2  43179  mzpcong  43417  dnnumch1  43489  aomclem1  43499  aomclem6  43504  lnr2i  43561  hbtlem5  43573  hbt  43575  rexanuz3  45543  choicefi  45646  suplesup  45784  xralrple2  45799  infxr  45811  infleinf  45816  xralrple4  45817  xralrple3  45818  xrralrecnnge  45834  supxrunb3  45843  supxrleubrnmpt  45849  unb2ltle  45858  suprleubrnmpt  45865  infxrgelbrnmpt  45897  supminfxr  45907  xrpnf  45928  islpcn  46082  limclner  46094  climd  46115  clim2d  46116  limsupmnflem  46163  limsupre3uzlem  46178  xlimpnfxnegmnf  46257  xlimxrre  46274  xlimmnfvlem1  46275  xlimmnfv  46277  xlimpnfvlem1  46279  xlimpnfv  46281  climxlim2lem  46288  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  fourierdlem103  46652  fourierdlem104  46653  etransclem48  46725  saluncl  46760  subsaliuncllem  46800  sge0pnffigt  46839  omessle  46941  caragensplit  46943  omeunile  46948  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvle  47043  vonvolmbllem  47103  vonvolmbl  47104  pimdecfgtioc  47158  smfpreimalt  47174  smfpreimaltf  47179  smfpreimale  47197  smfpreimagt  47205  smfpreimage  47225  smfmullem4  47237  smfinflem  47260  iccpartrn  47905  iccpartiun  47909  icceuelpart  47911  lidldomn1  48722  ply1mulgsumlem2  48878  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  snlindsntor  48962  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdig  49114