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  24142  bcthlem5  25204  gausslemma2dlem6  27259  opreu2reuALT  32379  foresf1o  32406  abrexss  32414  iinabrex  32471  reff  33802  locfinreflem  33803  cmpcref  33813  zarclsiin  33834  ldgenpisyslem1  34126  voliune  34192  volfiniune  34193  reprpmtf1o  34590  bnj1366  34792  weiunfrlem  36425  heicant  37622  indexdom  37701  glbconxN  39345  pmapglbx  39736  pmapglb2xN  39739  mzpexpmpt  42706  uzwo4  45020  ralimralim  45048  eliinid  45078  suprnmpt  45141  wessf1ornlem  45152  disjinfi  45159  choicefi  45167  axccdom  45189  axccd  45196  rnmptlb  45210  rnmptbddlem  45211  rnmptbd2lem  45215  upbdrech  45276  ssfiunibd  45280  iuneqfzuzlem  45303  xrralrecnnle  45352  supxrunb3  45368  supxrleubrnmpt  45375  unb2ltle  45384  rexabslelem  45387  suprleubrnmpt  45391  uzublem  45399  infxrgelbrnmpt  45423  cvgcaule  45460  fprodcnlem  45570  limcrecl  45600  islpcn  45610  limsupre  45612  limcleqr  45615  0ellimcdiv  45620  limclner  45622  climinf2lem  45677  climinf3  45687  limsupmnflem  45691  limsupmnfuzlem  45697  limsupre3uzlem  45706  climisp  45717  climrescn  45719  climxrrelem  45720  climxrre  45721  climxlim2lem  45816  cncfshift  45845  cncfperiod  45850  cncfuni  45857  cncfioobd  45868  dvbdfbdioolem1  45899  dvnprodlem2  45918  stoweidlem28  45999  stoweidlem29  46000  stoweidlem31  46002  stoweidlem60  46031  stoweidlem62  46033  fourierdlem39  46117  fourierdlem68  46145  fourierdlem73  46150  fourierdlem77  46154  fourierdlem80  46157  fourierdlem83  46160  fourierdlem87  46164  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem113  46190  qndenserrnbllem  46265  dfsalgen2  46312  subsaliuncl  46329  sge0lefi  46369  sge0isum  46398  sge0reuzb  46419  iundjiun  46431  voliunsge0lem  46443  meaiuninclem  46451  meaiuninc3v  46455  isomenndlem  46501  ovnsubaddlem2  46542  hoidmvlelem3  46568  hoidmvlelem5  46570  hspdifhsp  46587  hoiqssbllem3  46595  hspmbllem2  46598  vonioo  46653  vonicc  46656  pimdecfgtioo  46688  issmflem  46698  issmfle  46716  issmfgt  46727  issmfgelem  46740  smflimlem2  46743  smfinflem  46788  smflimsuplem5  46795  smfliminflem  46801  fsupdm  46813  finfdm  46817  sbgoldbm  47758  sbgoldbo  47761  aacllem  49763