Theorem rspa 3221

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048

This theorem is referenced by:  r19.21bi  3224  mpteq12f  5174  reusv2lem2  5335  fompt  7051  frrlem12  8227  axdc4lem  10346  fprodle  15903  isucn2  24193  bcthlem5  25255  gausslemma2dlem6  27310  opreu2reuALT  32456  foresf1o  32484  abrexss  32492  iinabrex  32549  reff  33852  locfinreflem  33853  cmpcref  33863  zarclsiin  33884  ldgenpisyslem1  34176  voliune  34242  volfiniune  34243  reprpmtf1o  34639  bnj1366  34841  weiunfrlem  36508  heicant  37705  indexdom  37784  glbconxN  39487  pmapglbx  39878  pmapglb2xN  39881  mzpexpmpt  42848  uzwo4  45160  ralimralim  45188  eliinid  45218  suprnmpt  45281  wessf1ornlem  45292  disjinfi  45299  choicefi  45307  axccdom  45329  axccd  45336  rnmptlb  45350  rnmptbddlem  45351  rnmptbd2lem  45355  upbdrech  45416  ssfiunibd  45420  iuneqfzuzlem  45443  xrralrecnnle  45491  supxrunb3  45507  supxrleubrnmpt  45514  unb2ltle  45523  rexabslelem  45526  suprleubrnmpt  45530  uzublem  45538  infxrgelbrnmpt  45562  cvgcaule  45599  fprodcnlem  45709  limcrecl  45739  islpcn  45747  limsupre  45749  limcleqr  45752  0ellimcdiv  45757  limclner  45759  climinf2lem  45814  climinf3  45824  limsupmnflem  45828  limsupmnfuzlem  45834  limsupre3uzlem  45843  climisp  45854  climrescn  45856  climxrrelem  45857  climxrre  45858  climxlim2lem  45953  cncfshift  45982  cncfperiod  45987  cncfuni  45994  cncfioobd  46005  dvbdfbdioolem1  46036  dvnprodlem2  46055  stoweidlem28  46136  stoweidlem29  46137  stoweidlem31  46139  stoweidlem60  46168  stoweidlem62  46170  fourierdlem39  46254  fourierdlem68  46282  fourierdlem73  46287  fourierdlem77  46291  fourierdlem80  46294  fourierdlem83  46297  fourierdlem87  46301  fourierdlem94  46308  fourierdlem103  46317  fourierdlem104  46318  fourierdlem112  46326  fourierdlem113  46327  qndenserrnbllem  46402  dfsalgen2  46449  subsaliuncl  46466  sge0lefi  46506  sge0isum  46535  sge0reuzb  46556  iundjiun  46568  voliunsge0lem  46580  meaiuninclem  46588  meaiuninc3v  46592  isomenndlem  46638  ovnsubaddlem2  46679  hoidmvlelem3  46705  hoidmvlelem5  46707  hspdifhsp  46724  hoiqssbllem3  46732  hspmbllem2  46735  vonioo  46790  vonicc  46793  pimdecfgtioo  46825  issmflem  46835  issmfle  46853  issmfgt  46864  issmfgelem  46877  smflimlem2  46880  smfinflem  46925  smflimsuplem5  46932  smfliminflem  46938  fsupdm  46950  finfdm  46954  sbgoldbm  47894  sbgoldbo  47897  aacllem  49912