Theorem rspa 3246

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

Assertion

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

Proof of Theorem rspa

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063

This theorem is referenced by:  r19.21bi  3249  dfiun2gOLD  5033  mpteq12f  5235  reusv2lem2  5396  frrlem12  8277  axdc4lem  10446  fprodle  15936  isucn2  23766  bcthlem5  24827  gausslemma2dlem6  26855  opreu2reuALT  31695  foresf1o  31720  abrexss  31727  iinabrex  31778  reff  32757  locfinreflem  32758  cmpcref  32768  zarclsiin  32789  ldgenpisyslem1  33099  voliune  33165  volfiniune  33166  reprpmtf1o  33576  bnj1366  33778  heicant  36461  indexdom  36540  glbconxN  38187  pmapglbx  38578  pmapglb2xN  38581  mzpexpmpt  41416  uzwo4  43673  ralimralim  43703  eliinid  43733  suprnmpt  43803  wessf1ornlem  43815  fompt  43823  disjinfi  43824  choicefi  43832  axccdom  43854  axccd  43861  rnmptlb  43881  rnmptbddlem  43882  rnmptbd2lem  43887  upbdrech  43950  ssfiunibd  43954  iuneqfzuzlem  43979  xrralrecnnle  44028  supxrunb3  44044  supxrleubrnmpt  44051  unb2ltle  44060  rexabslelem  44063  suprleubrnmpt  44067  uzublem  44075  infxrgelbrnmpt  44099  cvgcaule  44137  fprodcnlem  44250  limcrecl  44280  islpcn  44290  limsupre  44292  limcleqr  44295  0ellimcdiv  44300  limclner  44302  climinf2lem  44357  climinf3  44367  limsupmnflem  44371  limsupmnfuzlem  44377  limsupre3uzlem  44386  climisp  44397  climrescn  44399  climxrrelem  44400  climxrre  44401  climxlim2lem  44496  cncfshift  44525  cncfperiod  44530  cncfuni  44537  cncfioobd  44548  dvbdfbdioolem1  44579  dvnprodlem2  44598  stoweidlem28  44679  stoweidlem29  44680  stoweidlem31  44682  stoweidlem60  44711  stoweidlem62  44713  fourierdlem39  44797  fourierdlem68  44825  fourierdlem73  44830  fourierdlem77  44834  fourierdlem80  44837  fourierdlem83  44840  fourierdlem87  44844  fourierdlem94  44851  fourierdlem103  44860  fourierdlem104  44861  fourierdlem112  44869  fourierdlem113  44870  qndenserrnbllem  44945  dfsalgen2  44992  subsaliuncl  45009  sge0lefi  45049  sge0isum  45078  sge0reuzb  45099  iundjiun  45111  voliunsge0lem  45123  meaiuninclem  45131  meaiuninc3v  45135  isomenndlem  45181  ovnsubaddlem2  45222  hoidmvlelem3  45248  hoidmvlelem5  45250  hspdifhsp  45267  hoiqssbllem3  45275  hspmbllem2  45278  vonioo  45333  vonicc  45336  pimdecfgtioo  45368  issmflem  45378  issmfle  45396  issmfgt  45407  issmfgelem  45420  smflimlem2  45423  smfinflem  45468  smflimsuplem5  45475  smfliminflem  45481  fsupdm  45493  finfdm  45497  sbgoldbm  46387  sbgoldbo  46390  aacllem  47750