Theorem rspcva 3583

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rexraleqim  3610  fvn0ssdmfun  7028  fveqdmss  7032  fvcofneq  7047  wfr3g  8275  boxriin  8890  boxcutc  8891  pwssfi  9118  marypha1lem  9360  supmo  9379  infmo  9424  unwdomg  9513  frr3g  9685  isinffi  9921  axdc3lem2  10380  grothac  10759  nqereu  10858  nnsub  12206  zextle  12583  xrsupsslem  13243  xrinfmsslem  13244  supxrunb1  13255  supxrunb2  13256  injresinjlem  13724  ssnn0fi  13926  suppssfz  13935  faclbnd4lem4  14237  ishashinf  14404  rexuz3  15291  cau3lem  15297  caubnd2  15300  o1co  15528  climcn1  15534  incexclem  15778  dvdsext  16267  mreintcl  17532  initoeu1  17953  initoeu2  17958  termoeu1  17960  lublecllem  18299  mgmidmo  18569  gsumval2  18595  dfgrp3lem  18952  symgfix2  19330  odeq  19464  gexid  19495  ringurd  20105  o2timesd  20130  rglcom4d  20131  gsummoncoe1  22228  m2detleiblem3  22549  m2detleiblem4  22550  cpmatmcllem  22638  mp2pm2mplem4  22729  cayleyhamilton1  22812  cmpsublem  23319  cmpsub  23320  cmpfii  23329  ptpjcn  23531  isufil2  23828  ufileu  23839  lmmbr  25191  caussi  25230  plyco0  26130  dgrco  26214  emcllem7  26945  isppw2  27058  addsrid  27911  mulsrid  28056  n0subs  28293  uvtxnbgrvtx  29373  rusgrnumwwlks  29954  clwwlkf  30026  vdgn1frgrv2  30275  frgrregorufr  30304  grpoidinvlem3  30485  grpoideu  30488  lnconi  32012  fsumiunle  32804  tpr2rico  33895  esumiun  34077  0elsiga  34097  sigaclci  34115  dya2icoseg2  34262  derangsn  35150  sat1el2xp  35359  fwddifnp1  36146  poimirlem25  37632  poimirlem26  37633  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  heicant  37642  mblfinlem2  37645  ftc1anc  37688  fdc  37732  bndss  37773  isdrngo2  37945  divrngidl  38015  maxidlmax  38030  cdleme0nex  40277  dihglblem2N  41281  hgmapvs  41878  ismrcd1  42679  nacsfg  42686  isnacs3  42691  nacsfix  42693  mzpcl1  42710  mzpcl2  42711  mzpcong  42954  dnnumch1  43026  aomclem1  43036  aomclem6  43041  lnr2i  43098  hbtlem5  43110  hbt  43112  rexanuz3  45083  choicefi  45187  fsneq  45193  suplesup  45328  xralrple2  45343  infxr  45356  infleinf  45361  xralrple4  45362  xralrple3  45363  xrralrecnnge  45379  supxrunb3  45388  supxrleubrnmpt  45395  unb2ltle  45404  suprleubrnmpt  45411  infxrgelbrnmpt  45443  supminfxr  45453  xrpnf  45474  islpcn  45630  limclner  45642  climd  45663  clim2d  45664  limsupmnflem  45711  limsupre3uzlem  45726  xlimpnfxnegmnf  45805  xlimxrre  45822  xlimmnfvlem1  45823  xlimmnfv  45825  xlimpnfvlem1  45827  xlimpnfv  45829  climxlim2lem  45836  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  fourierdlem103  46200  fourierdlem104  46201  etransclem48  46273  saluncl  46308  subsaliuncllem  46348  sge0pnffigt  46387  omessle  46489  caragensplit  46491  omeunile  46496  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvle  46591  vonvolmbllem  46651  vonvolmbl  46652  pimdecfgtioc  46706  smfpreimalt  46722  smfpreimaltf  46727  smfpreimale  46745  smfpreimagt  46753  smfpreimage  46773  smfmullem4  46785  smfinflem  46808  iccpartrn  47424  iccpartiun  47428  icceuelpart  47430  lidldomn1  48212  ply1mulgsumlem2  48369  lindslinindsimp2lem5  48444  lindslinindsimp2  48445  snlindsntor  48453  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  nn0sumshdig  48605