Theorem rspa 3231

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

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 2007  ax-12 2177

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

This theorem is referenced by:  r19.21bi  3234  dfiun2gOLD  5007  mpteq12f  5205  reusv2lem2  5369  fompt  7108  frrlem12  8296  axdc4lem  10469  fprodle  16012  isucn2  24217  bcthlem5  25280  gausslemma2dlem6  27335  opreu2reuALT  32458  foresf1o  32485  abrexss  32493  iinabrex  32550  reff  33870  locfinreflem  33871  cmpcref  33881  zarclsiin  33902  ldgenpisyslem1  34194  voliune  34260  volfiniune  34261  reprpmtf1o  34658  bnj1366  34860  weiunfrlem  36482  heicant  37679  indexdom  37758  glbconxN  39397  pmapglbx  39788  pmapglb2xN  39791  mzpexpmpt  42768  uzwo4  45077  ralimralim  45105  eliinid  45135  suprnmpt  45198  wessf1ornlem  45209  disjinfi  45216  choicefi  45224  axccdom  45246  axccd  45253  rnmptlb  45267  rnmptbddlem  45268  rnmptbd2lem  45272  upbdrech  45334  ssfiunibd  45338  iuneqfzuzlem  45361  xrralrecnnle  45410  supxrunb3  45426  supxrleubrnmpt  45433  unb2ltle  45442  rexabslelem  45445  suprleubrnmpt  45449  uzublem  45457  infxrgelbrnmpt  45481  cvgcaule  45518  fprodcnlem  45628  limcrecl  45658  islpcn  45668  limsupre  45670  limcleqr  45673  0ellimcdiv  45678  limclner  45680  climinf2lem  45735  climinf3  45745  limsupmnflem  45749  limsupmnfuzlem  45755  limsupre3uzlem  45764  climisp  45775  climrescn  45777  climxrrelem  45778  climxrre  45779  climxlim2lem  45874  cncfshift  45903  cncfperiod  45908  cncfuni  45915  cncfioobd  45926  dvbdfbdioolem1  45957  dvnprodlem2  45976  stoweidlem28  46057  stoweidlem29  46058  stoweidlem31  46060  stoweidlem60  46089  stoweidlem62  46091  fourierdlem39  46175  fourierdlem68  46203  fourierdlem73  46208  fourierdlem77  46212  fourierdlem80  46215  fourierdlem83  46218  fourierdlem87  46222  fourierdlem94  46229  fourierdlem103  46238  fourierdlem104  46239  fourierdlem112  46247  fourierdlem113  46248  qndenserrnbllem  46323  dfsalgen2  46370  subsaliuncl  46387  sge0lefi  46427  sge0isum  46456  sge0reuzb  46477  iundjiun  46489  voliunsge0lem  46501  meaiuninclem  46509  meaiuninc3v  46513  isomenndlem  46559  ovnsubaddlem2  46600  hoidmvlelem3  46626  hoidmvlelem5  46628  hspdifhsp  46645  hoiqssbllem3  46653  hspmbllem2  46656  vonioo  46711  vonicc  46714  pimdecfgtioo  46746  issmflem  46756  issmfle  46774  issmfgt  46785  issmfgelem  46798  smflimlem2  46801  smfinflem  46846  smflimsuplem5  46853  smfliminflem  46859  fsupdm  46871  finfdm  46875  sbgoldbm  47798  sbgoldbo  47801  aacllem  49665