Theorem rspa 3208

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145

This theorem is referenced by:  r19.21bi  3210  ralbiOLD  3235  ralrexbidOLD  3325  dfiun2g  4957  mpteq12f  5151  reusv2lem2  5302  axdc4lem  9879  fprodle  15352  isucn2  22890  bcthlem5  23933  gausslemma2dlem6  25950  opreu2reuALT  30242  foresf1o  30267  abrexss  30274  reff  31105  locfinreflem  31106  cmpcref  31116  ldgenpisyslem1  31424  voliune  31490  volfiniune  31491  reprpmtf1o  31899  bnj1366  32103  frrlem12  33136  heicant  34929  indexdom  35011  glbconxN  36516  pmapglbx  36907  pmapglb2xN  36910  mzpexpmpt  39349  uzwo4  41322  ralimralim  41352  eliinid  41384  ralimda  41413  suprnmpt  41437  wessf1ornlem  41452  fompt  41460  disjinfi  41461  choicefi  41470  axccdom  41494  axccd  41502  rnmptlb  41521  rnmptbddlem  41522  rnmptbd2lem  41527  upbdrech  41579  ssfiunibd  41583  iuneqfzuzlem  41609  xrralrecnnle  41660  supxrunb3  41679  supxrleubrnmpt  41686  unb2ltle  41696  rexabslelem  41699  suprleubrnmpt  41703  uzublem  41711  infxrgelbrnmpt  41737  fprodcnlem  41887  limcrecl  41917  islpcn  41927  limsupre  41929  limcleqr  41932  0ellimcdiv  41937  limclner  41939  climinf2lem  41994  climinf3  42004  limsupmnflem  42008  limsupmnfuzlem  42014  limsupre3uzlem  42023  climisp  42034  climrescn  42036  climxrrelem  42037  climxrre  42038  climxlim2lem  42133  cncfshift  42164  cncfperiod  42169  cncfuni  42176  cncfioobd  42187  dvbdfbdioolem1  42220  dvnprodlem2  42239  stoweidlem28  42320  stoweidlem29  42321  stoweidlem31  42323  stoweidlem60  42352  stoweidlem62  42354  fourierdlem39  42438  fourierdlem68  42466  fourierdlem73  42471  fourierdlem77  42475  fourierdlem80  42478  fourierdlem83  42481  fourierdlem87  42485  fourierdlem94  42492  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  fourierdlem113  42511  qndenserrnbllem  42586  dfsalgen2  42631  subsaliuncl  42648  sge0lefi  42687  sge0isum  42716  sge0reuzb  42737  iundjiun  42749  voliunsge0lem  42761  meaiuninclem  42769  meaiuninc3v  42773  isomenndlem  42819  ovnsubaddlem2  42860  hoidmvlelem3  42886  hoidmvlelem5  42888  hspdifhsp  42905  hoiqssbllem3  42913  hspmbllem2  42916  vonioo  42971  vonicc  42974  pimdecfgtioo  43002  issmflem  43011  issmfle  43029  issmfgt  43040  issmfgelem  43052  smflimlem2  43055  smfinflem  43098  smflimsuplem5  43105  smfliminflem  43111  sbgoldbm  43956  sbgoldbo  43959  aacllem  44909