Theorem rspa 3225

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

Assertion

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

Proof of Theorem rspa

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

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

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 2184

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

This theorem is referenced by:  r19.21bi  3228  mpteq12f  5183  reusv2lem2  5344  fompt  7063  frrlem12  8239  axdc4lem  10365  fprodle  15919  isucn2  24222  bcthlem5  25284  gausslemma2dlem6  27339  opreu2reuALT  32551  foresf1o  32579  abrexss  32587  iinabrex  32644  reff  33996  locfinreflem  33997  cmpcref  34007  zarclsiin  34028  ldgenpisyslem1  34320  voliune  34386  volfiniune  34387  reprpmtf1o  34783  bnj1366  34985  weiunfrlem  36658  heicant  37852  indexdom  37931  glbconxN  39634  pmapglbx  40025  pmapglb2xN  40028  mzpexpmpt  42983  uzwo4  45294  ralimralim  45322  eliinid  45351  suprnmpt  45414  wessf1ornlem  45425  disjinfi  45432  choicefi  45440  axccdom  45462  axccd  45469  rnmptlb  45483  rnmptbddlem  45484  rnmptbd2lem  45488  upbdrech  45549  ssfiunibd  45553  iuneqfzuzlem  45575  xrralrecnnle  45623  supxrunb3  45639  supxrleubrnmpt  45646  unb2ltle  45655  rexabslelem  45658  suprleubrnmpt  45662  uzublem  45670  infxrgelbrnmpt  45694  cvgcaule  45731  fprodcnlem  45841  limcrecl  45871  islpcn  45879  limsupre  45881  limcleqr  45884  0ellimcdiv  45889  limclner  45891  climinf2lem  45946  climinf3  45956  limsupmnflem  45960  limsupmnfuzlem  45966  limsupre3uzlem  45975  climisp  45986  climrescn  45988  climxrrelem  45989  climxrre  45990  climxlim2lem  46085  cncfshift  46114  cncfperiod  46119  cncfuni  46126  cncfioobd  46137  dvbdfbdioolem1  46168  dvnprodlem2  46187  stoweidlem28  46268  stoweidlem29  46269  stoweidlem31  46271  stoweidlem60  46300  stoweidlem62  46302  fourierdlem39  46386  fourierdlem68  46414  fourierdlem73  46419  fourierdlem77  46423  fourierdlem80  46426  fourierdlem83  46429  fourierdlem87  46433  fourierdlem94  46440  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  fourierdlem113  46459  qndenserrnbllem  46534  dfsalgen2  46581  subsaliuncl  46598  sge0lefi  46638  sge0isum  46667  sge0reuzb  46688  iundjiun  46700  voliunsge0lem  46712  meaiuninclem  46720  meaiuninc3v  46724  isomenndlem  46770  ovnsubaddlem2  46811  hoidmvlelem3  46837  hoidmvlelem5  46839  hspdifhsp  46856  hoiqssbllem3  46864  hspmbllem2  46867  vonioo  46922  vonicc  46925  pimdecfgtioo  46957  issmflem  46967  issmfle  46985  issmfgt  46996  issmfgelem  47009  smflimlem2  47012  smfinflem  47057  smflimsuplem5  47064  smfliminflem  47070  fsupdm  47082  finfdm  47086  sbgoldbm  48026  sbgoldbo  48029  aacllem  50042