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 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  r19.21bi  3254  mpteq12f  5189  reusv2lem2  5361  fompt  7123  frrlem12  8323  axdc4lem  10540  fprodle  16172  isucn2  24606  bcthlem5  25658  gausslemma2dlem6  27708  opreu2reuALT  33124  foresf1o  33151  abrexss  33159  iinabrex  33214  reff  34521  locfinreflem  34522  cmpcref  34532  zarclsiin  34553  ldgenpisyslem1  34846  voliune  34912  volfiniune  34913  reprpmtf1o  35305  bnj1366  35509  weiunfrlem  37376  heicant  38710  indexdom  38805  glbconxN  40572  pmapglbx  40963  pmapglb2xN  40966  mzpexpmpt  43893  uzwo4  46206  ralimralim  46234  eliinid  46262  suprnmpt  46325  wessf1ornlem  46336  disjinfi  46343  choicefi  46350  axccdom  46371  axccd  46377  rnmptlb  46391  rnmptbddlem  46392  rnmptbd2lem  46396  upbdrech  46457  ssfiunibd  46461  iuneqfzuzlem  46482  xrralrecnnle  46530  supxrunb3  46546  supxrleubrnmpt  46552  unb2ltle  46561  rexabslelem  46564  suprleubrnmpt  46568  uzublem  46576  infxrgelbrnmpt  46600  cvgcaule  46637  fprodcnlem  46747  limcrecl  46777  islpcn  46785  limsupre  46787  limcleqr  46790  0ellimcdiv  46795  limclner  46797  climinf2lem  46852  climinf3  46862  limsupmnflem  46866  limsupmnfuzlem  46872  limsupre3uzlem  46881  climisp  46892  climrescn  46894  climxrrelem  46895  climxrre  46896  climxlim2lem  46991  cncfshift  47020  cncfperiod  47025  cncfuni  47032  cncfioobd  47043  dvbdfbdioolem1  47074  dvnprodlem2  47093  stoweidlem28  47174  stoweidlem29  47175  stoweidlem31  47177  stoweidlem60  47206  stoweidlem62  47208  fourierdlem39  47292  fourierdlem68  47320  fourierdlem73  47325  fourierdlem77  47329  fourierdlem80  47332  fourierdlem83  47335  fourierdlem87  47339  fourierdlem94  47346  fourierdlem103  47355  fourierdlem104  47356  fourierdlem112  47364  fourierdlem113  47365  qndenserrnbllem  47440  dfsalgen2  47487  subsaliuncl  47504  sge0lefi  47544  sge0isum  47573  sge0reuzb  47594  iundjiun  47606  voliunsge0lem  47618  meaiuninclem  47626  meaiuninc3v  47630  isomenndlem  47676  ovnsubaddlem2  47717  hoidmvlelem3  47743  hoidmvlelem5  47745  hspdifhsp  47762  hoiqssbllem3  47770  hspmbllem2  47773  vonioo  47828  vonicc  47831  pimdecfgtioo  47863  issmflem  47873  issmfle  47891  issmfgt  47902  issmfgelem  47915  smflimlem2  47918  smfinflem  47963  smflimsuplem5  47970  smfliminflem  47976  fsupdm  47988  finfdm  47992  sbgoldbm  49018  sbgoldbo  49021  aacllem  51150