Theorem rspa 3224

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  r19.21bi  3227  mpteq12f  5187  reusv2lem2  5349  fompt  7072  frrlem12  8253  axdc4lem  10384  fprodle  15938  isucn2  24199  bcthlem5  25261  gausslemma2dlem6  27316  opreu2reuALT  32456  foresf1o  32483  abrexss  32491  iinabrex  32548  reff  33822  locfinreflem  33823  cmpcref  33833  zarclsiin  33854  ldgenpisyslem1  34146  voliune  34212  volfiniune  34213  reprpmtf1o  34610  bnj1366  34812  weiunfrlem  36445  heicant  37642  indexdom  37721  glbconxN  39365  pmapglbx  39756  pmapglb2xN  39759  mzpexpmpt  42726  uzwo4  45040  ralimralim  45068  eliinid  45098  suprnmpt  45161  wessf1ornlem  45172  disjinfi  45179  choicefi  45187  axccdom  45209  axccd  45216  rnmptlb  45230  rnmptbddlem  45231  rnmptbd2lem  45235  upbdrech  45296  ssfiunibd  45300  iuneqfzuzlem  45323  xrralrecnnle  45372  supxrunb3  45388  supxrleubrnmpt  45395  unb2ltle  45404  rexabslelem  45407  suprleubrnmpt  45411  uzublem  45419  infxrgelbrnmpt  45443  cvgcaule  45480  fprodcnlem  45590  limcrecl  45620  islpcn  45630  limsupre  45632  limcleqr  45635  0ellimcdiv  45640  limclner  45642  climinf2lem  45697  climinf3  45707  limsupmnflem  45711  limsupmnfuzlem  45717  limsupre3uzlem  45726  climisp  45737  climrescn  45739  climxrrelem  45740  climxrre  45741  climxlim2lem  45836  cncfshift  45865  cncfperiod  45870  cncfuni  45877  cncfioobd  45888  dvbdfbdioolem1  45919  dvnprodlem2  45938  stoweidlem28  46019  stoweidlem29  46020  stoweidlem31  46022  stoweidlem60  46051  stoweidlem62  46053  fourierdlem39  46137  fourierdlem68  46165  fourierdlem73  46170  fourierdlem77  46174  fourierdlem80  46177  fourierdlem83  46180  fourierdlem87  46184  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  qndenserrnbllem  46285  dfsalgen2  46332  subsaliuncl  46349  sge0lefi  46389  sge0isum  46418  sge0reuzb  46439  iundjiun  46451  voliunsge0lem  46463  meaiuninclem  46471  meaiuninc3v  46475  isomenndlem  46521  ovnsubaddlem2  46562  hoidmvlelem3  46588  hoidmvlelem5  46590  hspdifhsp  46607  hoiqssbllem3  46615  hspmbllem2  46618  vonioo  46673  vonicc  46676  pimdecfgtioo  46708  issmflem  46718  issmfle  46736  issmfgt  46747  issmfgelem  46760  smflimlem2  46763  smfinflem  46808  smflimsuplem5  46815  smfliminflem  46821  fsupdm  46833  finfdm  46837  sbgoldbm  47778  sbgoldbo  47781  aacllem  49783