Theorem rspcva 3560

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  rexraleqim  3578  fvn0ssdmfun  6961  fveqdmss  6965  fvcofneq  6978  wfr3g  8147  boxriin  8737  boxcutc  8738  marypha1lem  9201  supmo  9220  infmo  9263  unwdomg  9352  frr3g  9523  isinffi  9759  axdc3lem2  10216  grothac  10595  nqereu  10694  nnsub  12026  zextle  12402  xrsupsslem  13050  xrinfmsslem  13051  supxrunb1  13062  supxrunb2  13063  injresinjlem  13516  ssnn0fi  13714  suppssfz  13723  faclbnd4lem4  14019  ishashinf  14186  rexuz3  15069  cau3lem  15075  caubnd2  15078  o1co  15304  climcn1  15310  incexclem  15557  dvdsext  16039  mreintcl  17313  initoeu1  17735  initoeu2  17740  termoeu1  17742  lublecllem  18087  mgmidmo  18353  gsumval2  18379  dfgrp3lem  18682  symgfix2  19033  odeq  19167  gexid  19195  gsummoncoe1  21484  m2detleiblem3  21787  m2detleiblem4  21788  cpmatmcllem  21876  mp2pm2mplem4  21967  cayleyhamilton1  22050  cmpsublem  22559  cmpsub  22560  cmpfii  22569  ptpjcn  22771  isufil2  23068  ufileu  23079  lmmbr  24431  caussi  24470  plyco0  25362  dgrco  25445  emcllem7  26160  isppw2  26273  uvtxnbgrvtx  27769  rusgrnumwwlks  28348  clwwlkf  28420  vdgn1frgrv2  28669  frgrregorufr  28698  grpoidinvlem3  28877  grpoideu  28880  lnconi  30404  fsumiunle  31152  rngurd  31491  tpr2rico  31871  esumiun  32071  0elsiga  32091  sigaclci  32109  dya2icoseg2  32254  derangsn  33141  sat1el2xp  33350  addsid1  34136  fwddifnp1  34476  poimirlem25  35811  poimirlem26  35812  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  heicant  35821  mblfinlem2  35824  ftc1anc  35867  fdc  35912  bndss  35953  isdrngo2  36125  divrngidl  36195  maxidlmax  36210  cdleme0nex  38311  dihglblem2N  39315  hgmapvs  39912  ismrcd1  40527  nacsfg  40534  isnacs3  40539  nacsfix  40541  mzpcl1  40558  mzpcl2  40559  mzpcong  40801  dnnumch1  40876  aomclem1  40886  aomclem6  40891  lnr2i  40948  hbtlem5  40960  hbt  40962  pwssfi  42600  rexanuz3  42653  choicefi  42747  fsneq  42753  suplesup  42885  xralrple2  42900  infxr  42913  infleinf  42918  xralrple4  42919  xralrple3  42920  xrralrecnnge  42937  supxrunb3  42946  supxrleubrnmpt  42953  unb2ltle  42962  suprleubrnmpt  42969  infxrgelbrnmpt  43001  supminfxr  43011  xrpnf  43033  islpcn  43187  limclner  43199  climd  43220  clim2d  43221  limsupmnflem  43268  limsupre3uzlem  43283  liminflelimsuplem  43323  xlimpnfxnegmnf  43362  xlimxrre  43379  xlimmnfvlem1  43380  xlimmnfv  43382  xlimpnfvlem1  43384  xlimpnfv  43386  climxlim2lem  43393  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  fourierdlem103  43757  fourierdlem104  43758  etransclem48  43830  saluncl  43865  subsaliuncllem  43903  sge0pnffigt  43941  omessle  44043  caragensplit  44045  omeunile  44050  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvle  44145  vonvolmbllem  44205  vonvolmbl  44206  pimdecfgtioc  44260  smfpreimalt  44276  smfpreimaltf  44281  smfpreimale  44299  smfpreimagt  44307  smfpreimage  44327  smfmullem4  44339  smfinflem  44361  iccpartrn  44893  iccpartiun  44897  icceuelpart  44899  lidldomn1  45490  ply1mulgsumlem2  45739  lindslinindsimp2lem5  45814  lindslinindsimp2  45815  snlindsntor  45823  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdig  45980