Theorem rspcva 3588

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 3586	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 411	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rexraleqim  3615  fsneq  7031  fvn0ssdmfun  7070  fveqdmss  7074  fvcofneq  7089  wfr3g  8315  boxriin  8937  boxcutc  8938  pwssfi  9160  marypha1lem  9392  supmo  9411  infmo  9456  unwdomg  9545  frr3g  9727  isinffi  9977  axdc3lem2  10434  grothac  10814  nqereu  10913  nnsub  12279  zextle  12668  xrsupsslem  13332  xrinfmsslem  13333  supxrunb1  13344  supxrunb2  13345  injresinjlem  13818  ssnn0fi  14020  suppssfz  14029  faclbnd4lem4  14331  ishashinf  14499  rexuz3  15399  cau3lem  15405  caubnd2  15408  o1co  15636  climcn1  15642  incexclem  15889  dvdsext  16378  mreintcl  17646  initoeu1  18067  initoeu2  18072  termoeu1  18074  lublecllem  18413  mgmidmo  18717  gsumval2  18743  dfgrp3lem  19103  symgfix2  19485  odeq  19619  gexid  19650  ringurd  20266  o2timesd  20291  rglcom4d  20292  gsummoncoe1  22436  m2detleiblem3  22754  m2detleiblem4  22755  cpmatmcllem  22843  mp2pm2mplem4  22934  cayleyhamilton1  23017  cmpsublem  23524  cmpsub  23525  cmpfii  23534  ptpjcn  23736  isufil2  24033  ufileu  24044  lmmbr  25385  caussi  25424  plyco0  26317  dgrco  26400  emcllem7  27131  isppw2  27244  addsrid  28122  mulsrid  28271  n0subs  28521  uvtxnbgrvtx  29683  rusgrnumwwlks  30266  clwwlkf  30338  vdgn1frgrv2  30587  frgrregorufr  30616  grpoidinvlem3  30798  grpoideu  30801  lnconi  32325  fsumiunle  33113  tpr2rico  34246  esumiun  34428  0elsiga  34448  sigaclci  34466  dya2icoseg2  34612  derangsn  35560  sat1el2xp  35769  fwddifnp1  36555  poimirlem25  38183  poimirlem26  38184  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  heicant  38193  mblfinlem2  38196  ftc1anc  38239  fdc  38283  bndss  38324  isdrngo2  38496  divrngidl  38566  maxidlmax  38581  cdleme0nex  40953  dihglblem2N  41957  hgmapvs  42554  ismrcd1  43320  nacsfg  43327  isnacs3  43332  nacsfix  43334  mzpcl1  43351  mzpcl2  43352  mzpcong  43590  dnnumch1  43662  aomclem1  43672  aomclem6  43677  lnr2i  43734  hbtlem5  43746  hbt  43748  rexanuz3  45705  choicefi  45808  suplesup  45946  xralrple2  45961  infxr  45973  infleinf  45978  xralrple4  45979  xralrple3  45980  xrralrecnnge  45996  supxrunb3  46005  supxrleubrnmpt  46011  unb2ltle  46020  suprleubrnmpt  46027  infxrgelbrnmpt  46059  supminfxr  46069  xrpnf  46090  islpcn  46244  limclner  46256  climd  46277  clim2d  46278  limsupmnflem  46325  limsupre3uzlem  46340  xlimpnfxnegmnf  46419  xlimxrre  46436  xlimmnfvlem1  46437  xlimmnfv  46439  xlimpnfvlem1  46441  xlimpnfv  46443  climxlim2lem  46450  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  fourierdlem103  46814  fourierdlem104  46815  etransclem48  46887  saluncl  46922  subsaliuncllem  46962  sge0pnffigt  47001  omessle  47103  caragensplit  47105  omeunile  47110  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvle  47205  vonvolmbllem  47265  vonvolmbl  47266  pimdecfgtioc  47320  smfpreimalt  47336  smfpreimaltf  47341  smfpreimale  47359  smfpreimagt  47367  smfpreimage  47387  smfmullem4  47399  smfinflem  47422  iccpartrn  48067  iccpartiun  48071  icceuelpart  48073  lidldomn1  48884  ply1mulgsumlem2  49051  lindslinindsimp2lem5  49126  lindslinindsimp2  49127  snlindsntor  49135  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0sumshdig  49287