Theorem rspa 3251

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

Assertion

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

Proof of Theorem rspa

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077

This theorem is used by:  r19.21bi  3254  mpteq12f  5190  reusv2lem2  5364  fompt  7112  frrlem12  8297  axdc4lem  10460  fprodle  16086  isucn2  24507  bcthlem5  25559  gausslemma2dlem6  27611  opreu2reuALT  32955  foresf1o  32982  abrexss  32990  iinabrex  33045  reff  34352  locfinreflem  34353  cmpcref  34363  zarclsiin  34384  ldgenpisyslem1  34677  voliune  34743  volfiniune  34744  reprpmtf1o  35137  bnj1366  35341  weiunfrlem  37086  heicant  38407  indexdom  38487  glbconxN  40254  pmapglbx  40645  pmapglb2xN  40648  mzpexpmpt  43593  uzwo4  45890  ralimralim  45918  eliinid  45946  suprnmpt  46009  wessf1ornlem  46020  disjinfi  46027  choicefi  46034  axccdom  46055  axccd  46061  rnmptlb  46075  rnmptbddlem  46076  rnmptbd2lem  46080  upbdrech  46141  ssfiunibd  46145  iuneqfzuzlem  46167  xrralrecnnle  46215  supxrunb3  46231  supxrleubrnmpt  46237  unb2ltle  46246  rexabslelem  46249  suprleubrnmpt  46253  uzublem  46261  infxrgelbrnmpt  46285  cvgcaule  46322  fprodcnlem  46432  limcrecl  46462  islpcn  46470  limsupre  46472  limcleqr  46475  0ellimcdiv  46480  limclner  46482  climinf2lem  46537  climinf3  46547  limsupmnflem  46551  limsupmnfuzlem  46557  limsupre3uzlem  46566  climisp  46577  climrescn  46579  climxrrelem  46580  climxrre  46581  climxlim2lem  46676  cncfshift  46705  cncfperiod  46710  cncfuni  46717  cncfioobd  46728  dvbdfbdioolem1  46759  dvnprodlem2  46778  stoweidlem28  46859  stoweidlem29  46860  stoweidlem31  46862  stoweidlem60  46891  stoweidlem62  46893  fourierdlem39  46977  fourierdlem68  47005  fourierdlem73  47010  fourierdlem77  47014  fourierdlem80  47017  fourierdlem83  47020  fourierdlem87  47024  fourierdlem94  47031  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem113  47050  qndenserrnbllem  47125  dfsalgen2  47172  subsaliuncl  47189  sge0lefi  47229  sge0isum  47258  sge0reuzb  47279  iundjiun  47291  voliunsge0lem  47303  meaiuninclem  47311  meaiuninc3v  47315  isomenndlem  47361  ovnsubaddlem2  47402  hoidmvlelem3  47428  hoidmvlelem5  47430  hspdifhsp  47447  hoiqssbllem3  47455  hspmbllem2  47458  vonioo  47513  vonicc  47516  pimdecfgtioo  47548  issmflem  47558  issmfle  47576  issmfgt  47587  issmfgelem  47600  smflimlem2  47603  smfinflem  47648  smflimsuplem5  47655  smfliminflem  47661  fsupdm  47673  finfdm  47677  sbgoldbm  48703  sbgoldbo  48706  aacllem  50775