Theorem rspa 3226

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

Assertion

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

Proof of Theorem rspa

Step	Hyp	Ref	Expression
1		rsp 3225	. 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  3229  dfiun2gOLD  4995  mpteq12f  5192  reusv2lem2  5354  fompt  7090  frrlem12  8276  axdc4lem  10408  fprodle  15962  isucn2  24166  bcthlem5  25228  gausslemma2dlem6  27283  opreu2reuALT  32406  foresf1o  32433  abrexss  32441  iinabrex  32498  reff  33829  locfinreflem  33830  cmpcref  33840  zarclsiin  33861  ldgenpisyslem1  34153  voliune  34219  volfiniune  34220  reprpmtf1o  34617  bnj1366  34819  weiunfrlem  36452  heicant  37649  indexdom  37728  glbconxN  39372  pmapglbx  39763  pmapglb2xN  39766  mzpexpmpt  42733  uzwo4  45047  ralimralim  45075  eliinid  45105  suprnmpt  45168  wessf1ornlem  45179  disjinfi  45186  choicefi  45194  axccdom  45216  axccd  45223  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  upbdrech  45303  ssfiunibd  45307  iuneqfzuzlem  45330  xrralrecnnle  45379  supxrunb3  45395  supxrleubrnmpt  45402  unb2ltle  45411  rexabslelem  45414  suprleubrnmpt  45418  uzublem  45426  infxrgelbrnmpt  45450  cvgcaule  45487  fprodcnlem  45597  limcrecl  45627  islpcn  45637  limsupre  45639  limcleqr  45642  0ellimcdiv  45647  limclner  45649  climinf2lem  45704  climinf3  45714  limsupmnflem  45718  limsupmnfuzlem  45724  limsupre3uzlem  45733  climisp  45744  climrescn  45746  climxrrelem  45747  climxrre  45748  climxlim2lem  45843  cncfshift  45872  cncfperiod  45877  cncfuni  45884  cncfioobd  45895  dvbdfbdioolem1  45926  dvnprodlem2  45945  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem60  46058  stoweidlem62  46060  fourierdlem39  46144  fourierdlem68  46172  fourierdlem73  46177  fourierdlem77  46181  fourierdlem80  46184  fourierdlem83  46187  fourierdlem87  46191  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  qndenserrnbllem  46292  dfsalgen2  46339  subsaliuncl  46356  sge0lefi  46396  sge0isum  46425  sge0reuzb  46446  iundjiun  46458  voliunsge0lem  46470  meaiuninclem  46478  meaiuninc3v  46482  isomenndlem  46528  ovnsubaddlem2  46569  hoidmvlelem3  46595  hoidmvlelem5  46597  hspdifhsp  46614  hoiqssbllem3  46622  hspmbllem2  46625  vonioo  46680  vonicc  46683  pimdecfgtioo  46715  issmflem  46725  issmfle  46743  issmfgt  46754  issmfgelem  46767  smflimlem2  46770  smfinflem  46815  smflimsuplem5  46822  smfliminflem  46828  fsupdm  46840  finfdm  46844  sbgoldbm  47785  sbgoldbo  47788  aacllem  49790