Theorem rspa 3132

Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
rspa	⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)

Proof of Theorem rspa

Step	Hyp	Ref	Expression
1		rsp 3131	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
2	1	imp 407	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069

This theorem is referenced by:  r19.21bi  3134  ralimda  3431  dfiun2gOLD  4961  mpteq12f  5162  reusv2lem2  5322  frrlem12  8113  axdc4lem  10211  fprodle  15706  isucn2  23431  bcthlem5  24492  gausslemma2dlem6  26520  opreu2reuALT  30825  foresf1o  30850  abrexss  30857  iinabrex  30908  reff  31789  locfinreflem  31790  cmpcref  31800  zarclsiin  31821  ldgenpisyslem1  32131  voliune  32197  volfiniune  32198  reprpmtf1o  32606  bnj1366  32809  heicant  35812  indexdom  35892  glbconxN  37392  pmapglbx  37783  pmapglb2xN  37786  mzpexpmpt  40567  uzwo4  42601  ralimralim  42631  eliinid  42661  suprnmpt  42710  wessf1ornlem  42722  fompt  42730  disjinfi  42731  choicefi  42740  axccdom  42762  axccd  42768  rnmptlb  42788  rnmptbddlem  42789  rnmptbd2lem  42794  upbdrech  42844  ssfiunibd  42848  iuneqfzuzlem  42873  xrralrecnnle  42922  supxrunb3  42939  supxrleubrnmpt  42946  unb2ltle  42955  rexabslelem  42958  suprleubrnmpt  42962  uzublem  42970  infxrgelbrnmpt  42994  fprodcnlem  43140  limcrecl  43170  islpcn  43180  limsupre  43182  limcleqr  43185  0ellimcdiv  43190  limclner  43192  climinf2lem  43247  climinf3  43257  limsupmnflem  43261  limsupmnfuzlem  43267  limsupre3uzlem  43276  climisp  43287  climrescn  43289  climxrrelem  43290  climxrre  43291  climxlim2lem  43386  cncfshift  43415  cncfperiod  43420  cncfuni  43427  cncfioobd  43438  dvbdfbdioolem1  43469  dvnprodlem2  43488  stoweidlem28  43569  stoweidlem29  43570  stoweidlem31  43572  stoweidlem60  43601  stoweidlem62  43603  fourierdlem39  43687  fourierdlem68  43715  fourierdlem73  43720  fourierdlem77  43724  fourierdlem80  43727  fourierdlem83  43730  fourierdlem87  43734  fourierdlem94  43741  fourierdlem103  43750  fourierdlem104  43751  fourierdlem112  43759  fourierdlem113  43760  qndenserrnbllem  43835  dfsalgen2  43880  subsaliuncl  43897  sge0lefi  43936  sge0isum  43965  sge0reuzb  43986  iundjiun  43998  voliunsge0lem  44010  meaiuninclem  44018  meaiuninc3v  44022  isomenndlem  44068  ovnsubaddlem2  44109  hoidmvlelem3  44135  hoidmvlelem5  44137  hspdifhsp  44154  hoiqssbllem3  44162  hspmbllem2  44165  vonioo  44220  vonicc  44223  pimdecfgtioo  44254  issmflem  44263  issmfle  44281  issmfgt  44292  issmfgelem  44304  smflimlem2  44307  smfinflem  44350  smflimsuplem5  44357  smfliminflem  44363  sbgoldbm  45236  sbgoldbo  45239  aacllem  46505