Theorem rspa 3256

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

Assertion

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

Proof of Theorem rspa

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

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

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 2216

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

This theorem is used by:  r19.21bi  3259  mpteq12f  5198  reusv2lem2  5372  fompt  7117  frrlem12  8300  axdc4lem  10454  fprodle  16073  isucn2  24486  bcthlem5  25538  gausslemma2dlem6  27587  opreu2reuALT  32894  foresf1o  32921  abrexss  32929  iinabrex  32985  reff  34293  locfinreflem  34294  cmpcref  34304  zarclsiin  34325  ldgenpisyslem1  34618  voliune  34684  volfiniune  34685  reprpmtf1o  35078  bnj1366  35282  weiunfrlem  37032  heicant  38363  indexdom  38443  glbconxN  40210  pmapglbx  40601  pmapglb2xN  40604  mzpexpmpt  43534  uzwo4  45831  ralimralim  45859  eliinid  45887  suprnmpt  45950  wessf1ornlem  45961  disjinfi  45968  choicefi  45975  axccdom  45996  axccd  46002  rnmptlb  46016  rnmptbddlem  46017  rnmptbd2lem  46021  upbdrech  46082  ssfiunibd  46086  iuneqfzuzlem  46108  xrralrecnnle  46156  supxrunb3  46172  supxrleubrnmpt  46178  unb2ltle  46187  rexabslelem  46190  suprleubrnmpt  46194  uzublem  46202  infxrgelbrnmpt  46226  cvgcaule  46263  fprodcnlem  46373  limcrecl  46403  islpcn  46411  limsupre  46413  limcleqr  46416  0ellimcdiv  46421  limclner  46423  climinf2lem  46478  climinf3  46488  limsupmnflem  46492  limsupmnfuzlem  46498  limsupre3uzlem  46507  climisp  46518  climrescn  46520  climxrrelem  46521  climxrre  46522  climxlim2lem  46617  cncfshift  46646  cncfperiod  46651  cncfuni  46658  cncfioobd  46669  dvbdfbdioolem1  46700  dvnprodlem2  46719  stoweidlem28  46800  stoweidlem29  46801  stoweidlem31  46803  stoweidlem60  46832  stoweidlem62  46834  fourierdlem39  46918  fourierdlem68  46946  fourierdlem73  46951  fourierdlem77  46955  fourierdlem80  46958  fourierdlem83  46961  fourierdlem87  46965  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  fourierdlem113  46991  qndenserrnbllem  47066  dfsalgen2  47113  subsaliuncl  47130  sge0lefi  47170  sge0isum  47199  sge0reuzb  47220  iundjiun  47232  voliunsge0lem  47244  meaiuninclem  47252  meaiuninc3v  47256  isomenndlem  47302  ovnsubaddlem2  47343  hoidmvlelem3  47369  hoidmvlelem5  47371  hspdifhsp  47388  hoiqssbllem3  47396  hspmbllem2  47399  vonioo  47454  vonicc  47457  pimdecfgtioo  47489  issmflem  47499  issmfle  47517  issmfgt  47528  issmfgelem  47541  smflimlem2  47544  smfinflem  47589  smflimsuplem5  47596  smfliminflem  47602  fsupdm  47614  finfdm  47618  sbgoldbm  48607  sbgoldbo  48610  aacllem  50678