Theorem rspa 3255

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

Assertion

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

Proof of Theorem rspa

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

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

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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  r19.21bi  3258  mpteq12f  5196  reusv2lem2  5368  fompt  7150  frrlem12  8353  axdc4lem  10572  fprodle  16207  isucn2  24652  bcthlem5  25704  gausslemma2dlem6  27756  opreu2reuALT  33172  foresf1o  33199  abrexss  33207  iinabrex  33261  reff  34582  locfinreflem  34583  cmpcref  34593  zarclsiin  34614  ldgenpisyslem1  34907  voliune  34973  volfiniune  34974  reprpmtf1o  35366  bnj1366  35570  weiunfrlem  37467  heicant  38841  indexdom  38936  glbconxN  40701  pmapglbx  41092  pmapglb2xN  41095  mzpexpmpt  44022  uzwo4  46344  ralimralim  46371  eliinid  46399  suprnmpt  46462  wessf1ornlem  46473  disjinfi  46480  choicefi  46487  axccdom  46508  axccd  46514  rnmptlb  46528  rnmptbddlem  46529  rnmptbd2lem  46533  upbdrech  46594  ssfiunibd  46598  iuneqfzuzlem  46619  xrralrecnnle  46667  supxrunb3  46683  supxrleubrnmpt  46689  unb2ltle  46698  rexabslelem  46701  suprleubrnmpt  46705  uzublem  46713  infxrgelbrnmpt  46737  cvgcaule  46774  fprodcnlem  46884  limcrecl  46914  islpcn  46922  limsupre  46924  limcleqr  46927  0ellimcdiv  46932  limclner  46934  climinf2lem  46989  climinf3  46999  limsupmnflem  47003  limsupmnfuzlem  47009  limsupre3uzlem  47018  climisp  47029  climrescn  47031  climxrrelem  47032  climxrre  47033  climxlim2lem  47128  cncfshift  47157  cncfperiod  47162  cncfuni  47169  cncfioobd  47180  dvbdfbdioolem1  47211  dvnprodlem2  47230  stoweidlem28  47311  stoweidlem29  47312  stoweidlem31  47314  stoweidlem60  47343  stoweidlem62  47345  fourierdlem39  47429  fourierdlem68  47457  fourierdlem73  47462  fourierdlem77  47466  fourierdlem80  47469  fourierdlem83  47472  fourierdlem87  47476  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  fourierdlem113  47502  qndenserrnbllem  47577  dfsalgen2  47624  subsaliuncl  47641  sge0lefi  47681  sge0isum  47710  sge0reuzb  47731  iundjiun  47743  voliunsge0lem  47755  meaiuninclem  47763  meaiuninc3v  47767  isomenndlem  47813  ovnsubaddlem2  47854  hoidmvlelem3  47880  hoidmvlelem5  47882  hspdifhsp  47899  hoiqssbllem3  47907  hspmbllem2  47910  vonioo  47965  vonicc  47968  pimdecfgtioo  48000  issmflem  48010  issmfle  48028  issmfgt  48039  issmfgelem  48052  smflimlem2  48055  smfinflem  48100  smflimsuplem5  48107  smfliminflem  48113  fsupdm  48125  finfdm  48129  sbgoldbm  49155  sbgoldbo  49158  aacllem  51367