Theorem rspcva 3610

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rexraleqim  3634  fvn0ssdmfun  7073  fveqdmss  7077  fvcofneq  7091  wfr3g  8303  boxriin  8930  boxcutc  8931  marypha1lem  9424  supmo  9443  infmo  9486  unwdomg  9575  frr3g  9747  isinffi  9983  axdc3lem2  10442  grothac  10821  nqereu  10920  nnsub  12252  zextle  12631  xrsupsslem  13282  xrinfmsslem  13283  supxrunb1  13294  supxrunb2  13295  injresinjlem  13748  ssnn0fi  13946  suppssfz  13955  faclbnd4lem4  14252  ishashinf  14420  rexuz3  15291  cau3lem  15297  caubnd2  15300  o1co  15526  climcn1  15532  incexclem  15778  dvdsext  16260  mreintcl  17535  initoeu1  17957  initoeu2  17962  termoeu1  17964  lublecllem  18309  mgmidmo  18575  gsumval2  18601  dfgrp3lem  18917  symgfix2  19278  odeq  19412  gexid  19443  o2timesd  20026  rglcom4d  20027  gsummoncoe1  21819  m2detleiblem3  22122  m2detleiblem4  22123  cpmatmcllem  22211  mp2pm2mplem4  22302  cayleyhamilton1  22385  cmpsublem  22894  cmpsub  22895  cmpfii  22904  ptpjcn  23106  isufil2  23403  ufileu  23414  lmmbr  24766  caussi  24805  plyco0  25697  dgrco  25780  emcllem7  26495  isppw2  26608  addsrid  27437  mulsrid  27558  uvtxnbgrvtx  28639  rusgrnumwwlks  29217  clwwlkf  29289  vdgn1frgrv2  29538  frgrregorufr  29567  grpoidinvlem3  29746  grpoideu  29749  lnconi  31273  fsumiunle  32022  rngurd  32367  tpr2rico  32880  esumiun  33080  0elsiga  33100  sigaclci  33118  dya2icoseg2  33265  derangsn  34149  sat1el2xp  34358  fwddifnp1  35125  poimirlem25  36501  poimirlem26  36502  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  heicant  36511  mblfinlem2  36514  ftc1anc  36557  fdc  36601  bndss  36642  isdrngo2  36814  divrngidl  36884  maxidlmax  36899  cdleme0nex  39149  dihglblem2N  40153  hgmapvs  40750  ismrcd1  41421  nacsfg  41428  isnacs3  41433  nacsfix  41435  mzpcl1  41452  mzpcl2  41453  mzpcong  41696  dnnumch1  41771  aomclem1  41781  aomclem6  41786  lnr2i  41843  hbtlem5  41855  hbt  41857  pwssfi  43717  rexanuz3  43770  choicefi  43884  fsneq  43890  suplesup  44035  xralrple2  44050  infxr  44063  infleinf  44068  xralrple4  44069  xralrple3  44070  xrralrecnnge  44086  supxrunb3  44095  supxrleubrnmpt  44102  unb2ltle  44111  suprleubrnmpt  44118  infxrgelbrnmpt  44150  supminfxr  44160  xrpnf  44182  islpcn  44341  limclner  44353  climd  44374  clim2d  44375  limsupmnflem  44422  limsupre3uzlem  44437  liminflelimsuplem  44477  xlimpnfxnegmnf  44516  xlimxrre  44533  xlimmnfvlem1  44534  xlimmnfv  44536  xlimpnfvlem1  44538  xlimpnfv  44540  climxlim2lem  44547  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  fourierdlem103  44911  fourierdlem104  44912  etransclem48  44984  saluncl  45019  subsaliuncllem  45059  sge0pnffigt  45098  omessle  45200  caragensplit  45202  omeunile  45207  hoidmvlelem2  45298  hoidmvlelem3  45299  hoidmvle  45302  vonvolmbllem  45362  vonvolmbl  45363  pimdecfgtioc  45417  smfpreimalt  45433  smfpreimaltf  45438  smfpreimale  45456  smfpreimagt  45464  smfpreimage  45484  smfmullem4  45496  smfinflem  45519  iccpartrn  46084  iccpartiun  46088  icceuelpart  46090  lidldomn1  46776  ply1mulgsumlem2  47021  lindslinindsimp2lem5  47096  lindslinindsimp2  47097  snlindsntor  47105  nn0sumshdiglemA  47258  nn0sumshdiglemB  47259  nn0sumshdig  47262