Theorem rspcva 3589

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rexraleqim  3616  fvn0ssdmfun  7049  fveqdmss  7053  fvcofneq  7068  wfr3g  8301  boxriin  8916  boxcutc  8917  pwssfi  9147  marypha1lem  9391  supmo  9410  infmo  9455  unwdomg  9544  frr3g  9716  isinffi  9952  axdc3lem2  10411  grothac  10790  nqereu  10889  nnsub  12237  zextle  12614  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  injresinjlem  13755  ssnn0fi  13957  suppssfz  13966  faclbnd4lem4  14268  ishashinf  14435  rexuz3  15322  cau3lem  15328  caubnd2  15331  o1co  15559  climcn1  15565  incexclem  15809  dvdsext  16298  mreintcl  17563  initoeu1  17980  initoeu2  17985  termoeu1  17987  lublecllem  18326  mgmidmo  18594  gsumval2  18620  dfgrp3lem  18977  symgfix2  19353  odeq  19487  gexid  19518  ringurd  20101  o2timesd  20126  rglcom4d  20127  gsummoncoe1  22202  m2detleiblem3  22523  m2detleiblem4  22524  cpmatmcllem  22612  mp2pm2mplem4  22703  cayleyhamilton1  22786  cmpsublem  23293  cmpsub  23294  cmpfii  23303  ptpjcn  23505  isufil2  23802  ufileu  23813  lmmbr  25165  caussi  25204  plyco0  26104  dgrco  26188  emcllem7  26919  isppw2  27032  addsrid  27878  mulsrid  28023  n0subs  28260  uvtxnbgrvtx  29327  rusgrnumwwlks  29911  clwwlkf  29983  vdgn1frgrv2  30232  frgrregorufr  30261  grpoidinvlem3  30442  grpoideu  30445  lnconi  31969  fsumiunle  32761  tpr2rico  33909  esumiun  34091  0elsiga  34111  sigaclci  34129  dya2icoseg2  34276  derangsn  35164  sat1el2xp  35373  fwddifnp1  36160  poimirlem25  37646  poimirlem26  37647  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  heicant  37656  mblfinlem2  37659  ftc1anc  37702  fdc  37746  bndss  37787  isdrngo2  37959  divrngidl  38029  maxidlmax  38044  cdleme0nex  40291  dihglblem2N  41295  hgmapvs  41892  ismrcd1  42693  nacsfg  42700  isnacs3  42705  nacsfix  42707  mzpcl1  42724  mzpcl2  42725  mzpcong  42968  dnnumch1  43040  aomclem1  43050  aomclem6  43055  lnr2i  43112  hbtlem5  43124  hbt  43126  rexanuz3  45097  choicefi  45201  fsneq  45207  suplesup  45342  xralrple2  45357  infxr  45370  infleinf  45375  xralrple4  45376  xralrple3  45377  xrralrecnnge  45393  supxrunb3  45402  supxrleubrnmpt  45409  unb2ltle  45418  suprleubrnmpt  45425  infxrgelbrnmpt  45457  supminfxr  45467  xrpnf  45488  islpcn  45644  limclner  45656  climd  45677  clim2d  45678  limsupmnflem  45725  limsupre3uzlem  45740  xlimpnfxnegmnf  45819  xlimxrre  45836  xlimmnfvlem1  45837  xlimmnfv  45839  xlimpnfvlem1  45841  xlimpnfv  45843  climxlim2lem  45850  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  fourierdlem103  46214  fourierdlem104  46215  etransclem48  46287  saluncl  46322  subsaliuncllem  46362  sge0pnffigt  46401  omessle  46503  caragensplit  46505  omeunile  46510  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvle  46605  vonvolmbllem  46665  vonvolmbl  46666  pimdecfgtioc  46720  smfpreimalt  46736  smfpreimaltf  46741  smfpreimale  46759  smfpreimagt  46767  smfpreimage  46787  smfmullem4  46799  smfinflem  46822  iccpartrn  47435  iccpartiun  47439  icceuelpart  47441  lidldomn1  48223  ply1mulgsumlem2  48380  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  snlindsntor  48464  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdig  48616