Theorem rspa 3223

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

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 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050

This theorem is referenced by:  r19.21bi  3226  mpteq12f  5181  reusv2lem2  5342  fompt  7061  frrlem12  8237  axdc4lem  10363  fprodle  15917  isucn2  24220  bcthlem5  25282  gausslemma2dlem6  27337  opreu2reuALT  32500  foresf1o  32528  abrexss  32536  iinabrex  32593  reff  33945  locfinreflem  33946  cmpcref  33956  zarclsiin  33977  ldgenpisyslem1  34269  voliune  34335  volfiniune  34336  reprpmtf1o  34732  bnj1366  34934  weiunfrlem  36607  heicant  37795  indexdom  37874  glbconxN  39577  pmapglbx  39968  pmapglb2xN  39971  mzpexpmpt  42929  uzwo4  45240  ralimralim  45268  eliinid  45297  suprnmpt  45360  wessf1ornlem  45371  disjinfi  45378  choicefi  45386  axccdom  45408  axccd  45415  rnmptlb  45429  rnmptbddlem  45430  rnmptbd2lem  45434  upbdrech  45495  ssfiunibd  45499  iuneqfzuzlem  45521  xrralrecnnle  45569  supxrunb3  45585  supxrleubrnmpt  45592  unb2ltle  45601  rexabslelem  45604  suprleubrnmpt  45608  uzublem  45616  infxrgelbrnmpt  45640  cvgcaule  45677  fprodcnlem  45787  limcrecl  45817  islpcn  45825  limsupre  45827  limcleqr  45830  0ellimcdiv  45835  limclner  45837  climinf2lem  45892  climinf3  45902  limsupmnflem  45906  limsupmnfuzlem  45912  limsupre3uzlem  45921  climisp  45932  climrescn  45934  climxrrelem  45935  climxrre  45936  climxlim2lem  46031  cncfshift  46060  cncfperiod  46065  cncfuni  46072  cncfioobd  46083  dvbdfbdioolem1  46114  dvnprodlem2  46133  stoweidlem28  46214  stoweidlem29  46215  stoweidlem31  46217  stoweidlem60  46246  stoweidlem62  46248  fourierdlem39  46332  fourierdlem68  46360  fourierdlem73  46365  fourierdlem77  46369  fourierdlem80  46372  fourierdlem83  46375  fourierdlem87  46379  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  fourierdlem113  46405  qndenserrnbllem  46480  dfsalgen2  46527  subsaliuncl  46544  sge0lefi  46584  sge0isum  46613  sge0reuzb  46634  iundjiun  46646  voliunsge0lem  46658  meaiuninclem  46666  meaiuninc3v  46670  isomenndlem  46716  ovnsubaddlem2  46757  hoidmvlelem3  46783  hoidmvlelem5  46785  hspdifhsp  46802  hoiqssbllem3  46810  hspmbllem2  46813  vonioo  46868  vonicc  46871  pimdecfgtioo  46903  issmflem  46913  issmfle  46931  issmfgt  46942  issmfgelem  46955  smflimlem2  46958  smfinflem  47003  smflimsuplem5  47010  smfliminflem  47016  fsupdm  47028  finfdm  47032  sbgoldbm  47972  sbgoldbo  47975  aacllem  49988