Theorem rspa 3252

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

Assertion

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

Proof of Theorem rspa

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

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

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 3078

This theorem is used by:  r19.21bi  3255  mpteq12f  5190  reusv2lem2  5361  fompt  7116  frrlem12  8308  axdc4lem  10526  fprodle  16156  isucn2  24590  bcthlem5  25642  gausslemma2dlem6  27692  opreu2reuALT  33066  foresf1o  33093  abrexss  33101  iinabrex  33156  reff  34464  locfinreflem  34465  cmpcref  34475  zarclsiin  34496  ldgenpisyslem1  34789  voliune  34855  volfiniune  34856  reprpmtf1o  35248  bnj1366  35452  weiunfrlem  37232  heicant  38553  indexdom  38648  glbconxN  40415  pmapglbx  40806  pmapglb2xN  40809  mzpexpmpt  43735  uzwo4  46039  ralimralim  46067  eliinid  46095  suprnmpt  46158  wessf1ornlem  46169  disjinfi  46176  choicefi  46183  axccdom  46204  axccd  46210  rnmptlb  46224  rnmptbddlem  46225  rnmptbd2lem  46229  upbdrech  46290  ssfiunibd  46294  iuneqfzuzlem  46315  xrralrecnnle  46363  supxrunb3  46379  supxrleubrnmpt  46385  unb2ltle  46394  rexabslelem  46397  suprleubrnmpt  46401  uzublem  46409  infxrgelbrnmpt  46433  cvgcaule  46470  fprodcnlem  46580  limcrecl  46610  islpcn  46618  limsupre  46620  limcleqr  46623  0ellimcdiv  46628  limclner  46630  climinf2lem  46685  climinf3  46695  limsupmnflem  46699  limsupmnfuzlem  46705  limsupre3uzlem  46714  climisp  46725  climrescn  46727  climxrrelem  46728  climxrre  46729  climxlim2lem  46824  cncfshift  46853  cncfperiod  46858  cncfuni  46865  cncfioobd  46876  dvbdfbdioolem1  46907  dvnprodlem2  46926  stoweidlem28  47007  stoweidlem29  47008  stoweidlem31  47010  stoweidlem60  47039  stoweidlem62  47041  fourierdlem39  47125  fourierdlem68  47153  fourierdlem73  47158  fourierdlem77  47162  fourierdlem80  47165  fourierdlem83  47168  fourierdlem87  47172  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem113  47198  qndenserrnbllem  47273  dfsalgen2  47320  subsaliuncl  47337  sge0lefi  47377  sge0isum  47406  sge0reuzb  47427  iundjiun  47439  voliunsge0lem  47451  meaiuninclem  47459  meaiuninc3v  47463  isomenndlem  47509  ovnsubaddlem2  47550  hoidmvlelem3  47576  hoidmvlelem5  47578  hspdifhsp  47595  hoiqssbllem3  47603  hspmbllem2  47606  vonioo  47661  vonicc  47664  pimdecfgtioo  47696  issmflem  47706  issmfle  47724  issmfgt  47735  issmfgelem  47748  smflimlem2  47751  smfinflem  47796  smflimsuplem5  47803  smfliminflem  47809  fsupdm  47821  finfdm  47825  sbgoldbm  48851  sbgoldbo  48854  aacllem  50908