Theorem rspa 3227

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

Assertion

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

Proof of Theorem rspa

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

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

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 3046

This theorem is referenced by:  r19.21bi  3230  dfiun2gOLD  4998  mpteq12f  5195  reusv2lem2  5357  fompt  7093  frrlem12  8279  axdc4lem  10415  fprodle  15969  isucn2  24173  bcthlem5  25235  gausslemma2dlem6  27290  opreu2reuALT  32413  foresf1o  32440  abrexss  32448  iinabrex  32505  reff  33836  locfinreflem  33837  cmpcref  33847  zarclsiin  33868  ldgenpisyslem1  34160  voliune  34226  volfiniune  34227  reprpmtf1o  34624  bnj1366  34826  weiunfrlem  36459  heicant  37656  indexdom  37735  glbconxN  39379  pmapglbx  39770  pmapglb2xN  39773  mzpexpmpt  42740  uzwo4  45054  ralimralim  45082  eliinid  45112  suprnmpt  45175  wessf1ornlem  45186  disjinfi  45193  choicefi  45201  axccdom  45223  axccd  45230  rnmptlb  45244  rnmptbddlem  45245  rnmptbd2lem  45249  upbdrech  45310  ssfiunibd  45314  iuneqfzuzlem  45337  xrralrecnnle  45386  supxrunb3  45402  supxrleubrnmpt  45409  unb2ltle  45418  rexabslelem  45421  suprleubrnmpt  45425  uzublem  45433  infxrgelbrnmpt  45457  cvgcaule  45494  fprodcnlem  45604  limcrecl  45634  islpcn  45644  limsupre  45646  limcleqr  45649  0ellimcdiv  45654  limclner  45656  climinf2lem  45711  climinf3  45721  limsupmnflem  45725  limsupmnfuzlem  45731  limsupre3uzlem  45740  climisp  45751  climrescn  45753  climxrrelem  45754  climxrre  45755  climxlim2lem  45850  cncfshift  45879  cncfperiod  45884  cncfuni  45891  cncfioobd  45902  dvbdfbdioolem1  45933  dvnprodlem2  45952  stoweidlem28  46033  stoweidlem29  46034  stoweidlem31  46036  stoweidlem60  46065  stoweidlem62  46067  fourierdlem39  46151  fourierdlem68  46179  fourierdlem73  46184  fourierdlem77  46188  fourierdlem80  46191  fourierdlem83  46194  fourierdlem87  46198  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  qndenserrnbllem  46299  dfsalgen2  46346  subsaliuncl  46363  sge0lefi  46403  sge0isum  46432  sge0reuzb  46453  iundjiun  46465  voliunsge0lem  46477  meaiuninclem  46485  meaiuninc3v  46489  isomenndlem  46535  ovnsubaddlem2  46576  hoidmvlelem3  46602  hoidmvlelem5  46604  hspdifhsp  46621  hoiqssbllem3  46629  hspmbllem2  46632  vonioo  46687  vonicc  46690  pimdecfgtioo  46722  issmflem  46732  issmfle  46750  issmfgt  46761  issmfgelem  46774  smflimlem2  46777  smfinflem  46822  smflimsuplem5  46829  smfliminflem  46835  fsupdm  46847  finfdm  46851  sbgoldbm  47789  sbgoldbo  47792  aacllem  49794