Theorem rspa 3254

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080

This theorem is referenced by:  r19.21bi  3257  mpteq12f  5196  reusv2lem2  5370  fompt  7113  frrlem12  8290  axdc4lem  10434  fprodle  16046  isucn2  24435  bcthlem5  25487  gausslemma2dlem6  27536  opreu2reuALT  32823  foresf1o  32850  abrexss  32858  iinabrex  32914  reff  34229  locfinreflem  34230  cmpcref  34240  zarclsiin  34261  ldgenpisyslem1  34553  voliune  34619  volfiniune  34620  reprpmtf1o  35013  bnj1366  35217  weiunfrlem  36975  heicant  38306  indexdom  38385  glbconxN  40152  pmapglbx  40543  pmapglb2xN  40546  mzpexpmpt  43476  uzwo4  45773  ralimralim  45801  eliinid  45829  suprnmpt  45892  wessf1ornlem  45903  disjinfi  45910  choicefi  45917  axccdom  45938  axccd  45944  rnmptlb  45958  rnmptbddlem  45959  rnmptbd2lem  45963  upbdrech  46024  ssfiunibd  46028  iuneqfzuzlem  46050  xrralrecnnle  46098  supxrunb3  46114  supxrleubrnmpt  46120  unb2ltle  46129  rexabslelem  46132  suprleubrnmpt  46136  uzublem  46144  infxrgelbrnmpt  46168  cvgcaule  46205  fprodcnlem  46315  limcrecl  46345  islpcn  46353  limsupre  46355  limcleqr  46358  0ellimcdiv  46363  limclner  46365  climinf2lem  46420  climinf3  46430  limsupmnflem  46434  limsupmnfuzlem  46440  limsupre3uzlem  46449  climisp  46460  climrescn  46462  climxrrelem  46463  climxrre  46464  climxlim2lem  46559  cncfshift  46588  cncfperiod  46593  cncfuni  46600  cncfioobd  46611  dvbdfbdioolem1  46642  dvnprodlem2  46661  stoweidlem28  46742  stoweidlem29  46743  stoweidlem31  46745  stoweidlem60  46774  stoweidlem62  46776  fourierdlem39  46860  fourierdlem68  46888  fourierdlem73  46893  fourierdlem77  46897  fourierdlem80  46900  fourierdlem83  46903  fourierdlem87  46907  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem112  46932  fourierdlem113  46933  qndenserrnbllem  47008  dfsalgen2  47055  subsaliuncl  47072  sge0lefi  47112  sge0isum  47141  sge0reuzb  47162  iundjiun  47174  voliunsge0lem  47186  meaiuninclem  47194  meaiuninc3v  47198  isomenndlem  47244  ovnsubaddlem2  47285  hoidmvlelem3  47311  hoidmvlelem5  47313  hspdifhsp  47330  hoiqssbllem3  47338  hspmbllem2  47341  vonioo  47396  vonicc  47399  pimdecfgtioo  47431  issmflem  47441  issmfle  47459  issmfgt  47470  issmfgelem  47483  smflimlem2  47486  smfinflem  47531  smflimsuplem5  47538  smfliminflem  47544  fsupdm  47556  finfdm  47560  sbgoldbm  48549  sbgoldbo  48552  aacllem  50621