Theorem rspa 3251

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

Assertion

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

Proof of Theorem rspa

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077

This theorem is used by:  r19.21bi  3254  mpteq12f  5190  reusv2lem2  5364  fompt  7111  frrlem12  8296  axdc4lem  10457  fprodle  16083  isucn2  24504  bcthlem5  25556  gausslemma2dlem6  27608  opreu2reuALT  32952  foresf1o  32979  abrexss  32987  iinabrex  33042  reff  34349  locfinreflem  34350  cmpcref  34360  zarclsiin  34381  ldgenpisyslem1  34674  voliune  34740  volfiniune  34741  reprpmtf1o  35134  bnj1366  35338  weiunfrlem  37083  heicant  38404  indexdom  38484  glbconxN  40251  pmapglbx  40642  pmapglb2xN  40645  mzpexpmpt  43590  uzwo4  45887  ralimralim  45915  eliinid  45943  suprnmpt  46006  wessf1ornlem  46017  disjinfi  46024  choicefi  46031  axccdom  46052  axccd  46058  rnmptlb  46072  rnmptbddlem  46073  rnmptbd2lem  46077  upbdrech  46138  ssfiunibd  46142  iuneqfzuzlem  46164  xrralrecnnle  46212  supxrunb3  46228  supxrleubrnmpt  46234  unb2ltle  46243  rexabslelem  46246  suprleubrnmpt  46250  uzublem  46258  infxrgelbrnmpt  46282  cvgcaule  46319  fprodcnlem  46429  limcrecl  46459  islpcn  46467  limsupre  46469  limcleqr  46472  0ellimcdiv  46477  limclner  46479  climinf2lem  46534  climinf3  46544  limsupmnflem  46548  limsupmnfuzlem  46554  limsupre3uzlem  46563  climisp  46574  climrescn  46576  climxrrelem  46577  climxrre  46578  climxlim2lem  46673  cncfshift  46702  cncfperiod  46707  cncfuni  46714  cncfioobd  46725  dvbdfbdioolem1  46756  dvnprodlem2  46775  stoweidlem28  46856  stoweidlem29  46857  stoweidlem31  46859  stoweidlem60  46888  stoweidlem62  46890  fourierdlem39  46974  fourierdlem68  47002  fourierdlem73  47007  fourierdlem77  47011  fourierdlem80  47014  fourierdlem83  47017  fourierdlem87  47021  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem113  47047  qndenserrnbllem  47122  dfsalgen2  47169  subsaliuncl  47186  sge0lefi  47226  sge0isum  47255  sge0reuzb  47276  iundjiun  47288  voliunsge0lem  47300  meaiuninclem  47308  meaiuninc3v  47312  isomenndlem  47358  ovnsubaddlem2  47399  hoidmvlelem3  47425  hoidmvlelem5  47427  hspdifhsp  47444  hoiqssbllem3  47452  hspmbllem2  47455  vonioo  47510  vonicc  47513  pimdecfgtioo  47545  issmflem  47555  issmfle  47573  issmfgt  47584  issmfgelem  47597  smflimlem2  47600  smfinflem  47645  smflimsuplem5  47652  smfliminflem  47658  fsupdm  47670  finfdm  47674  sbgoldbm  48700  sbgoldbo  48703  aacllem  50772