Theorem nfra1 3288

Description: The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfra1	⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem nfra1

Step	Hyp	Ref	Expression
1		df-ral 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 2187	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1875	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1560  Ⅎwnf 1805   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-10 2177

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1802  df-nf 1806  df-ral 3079

This theorem is referenced by:  hbra1  3301  r19.12  3313  nfra2  3365  ralcom2  3366  2reu1  3852  nfss  3931  2reu4lem  4479  iuneqconst  4963  nfii1  4988  mpteq12f  5187  reusv1  5356  reusv2lem1  5357  reusv2lem2  5358  reusv2lem3  5359  ralxfrALT  5374  fvmptss  6990  fompt  7101  ffnfv  7102  riota5f  7383  mpoeq123  7470  tfinds  7842  zfrep6OLD  7938  frrlem4  8272  tfr3  8372  tz7.48-1  8416  tz7.49  8418  naddsuc2  8674  nfixp1  8902  nneneq  9176  scottex  9845  dfac2b  10089  infpssrlem4  10265  hsmexlem2  10386  hsmexlem4  10388  domtriomlem  10401  axdc3lem2  10410  axdc3lem4  10412  axdc4lem  10414  zorn2lem5  10459  konigthlem  10528  eltsk2g  10711  dedekind  11348  dedekindle  11349  lble  12146  fsuppmapnn0fiublem  14005  fsuppmapnn0fiub  14006  fsuppmapnn0fiubex  14007  prodeq2ii  15943  fprodle  16028  lcmfunsnlem1  16673  lcmfunsnlem2lem1  16674  lcmfunsnlem2  16676  mreiincl  17626  mreexexd  17682  catpropd  17743  acsmapd  18588  gsummatr01lem4  22720  cpmatmcllem  22780  alexsubALTlem3  24111  isucn2  24340  nosupbnd1  27780  noinfbnd1  27795  bdaypw2n0bndlem  28558  mpteleeOLD  29098  chirred  32600  opreu2reuALT  32678  foresf1o  32705  abrexss  32713  iinabrex  32771  aciunf1lem  32866  nn0min  33025  fprodex01  33029  isarchiofld  33381  elrspunidl  33616  vieta  33879  reff  34138  locfinreflem  34139  cmpcref  34149  zarcmplem  34180  esumcl  34329  measvunilem  34511  measvunilem0  34512  measvuni  34513  voliune  34528  volfiniune  34529  omssubadd  34599  bnj1366  35126  bnj1379  35127  bnj571  35203  bnj1039  35268  bnj1128  35287  bnj1204  35309  bnj1279  35315  bnj1307  35320  bnj1388  35330  bnj1398  35331  bnj1444  35340  bnj1489  35353  bnj1525  35366  dfon2lem3  36138  domalom  37903  ralssiun  37906  fvineqsneu  37910  fvineqsneq  37911  heicant  38159  cover2  38219  upixp  38233  indexdom  38238  filbcmb  38244  riotasvd  39585  riotasv2d  39586  riotasv2s  39587  glbconxN  40007  pmapglbx  40398  pmapglb2xN  40401  cdleme26ee  40989  cdlemefr29exN  41031  cdlemefs32sn1aw  41043  cdleme43fsv1snlem  41049  cdleme41sn3a  41062  cdleme32d  41073  cdleme32f  41075  cdleme40m  41096  cdleme40n  41097  cdlemk36  41542  cdlemk38  41544  cdlemkid  41565  cdlemk19x  41572  cdlemk11t  41575  mzpexpmpt  43331  nadd1suc  43974  gneispace  44715  mnuprdlem4  44856  ssralv2  45112  tratrb  45117  modelaxrep  45562  fnchoice  45614  rfcnnnub  45621  uzwo4  45638  ralimralim  45666  suprnmpt  45757  choicefi  45782  axccdom  45803  axccd  45809  rnmptlb  45823  rnmptbddlem  45824  rnmptbd2lem  45828  rnmptbdlem  45835  upbdrech  45889  ssfiunibd  45893  iuneqfzuzlem  45915  infxrunb2  45948  xrralrecnnle  45963  supxrunb3  45979  supxrleubrnmpt  45985  unb2ltle  45994  rexabslelem  45997  allbutfiinf  45999  suprleubrnmpt  46001  uzub  46010  infxrgelbrnmpt  46033  cvgcaule  46070  mccl  46179  climsuse  46189  mullimc  46197  islptre  46200  mullimcf  46204  limcrecl  46210  islpcn  46218  limsupre  46220  limcleqr  46223  addlimc  46227  0ellimcdiv  46228  limclner  46230  climinf2lem  46285  limsupubuz  46292  climinf3  46295  limsupmnflem  46299  limsupmnfuzlem  46305  limsupre3uzlem  46314  climisp  46325  climrescn  46327  climxrrelem  46328  climxrre  46329  xlimmnfv  46413  xlimpnfv  46417  climxlim2lem  46424  cncfioobd  46476  stoweidlem16  46595  stoweidlem28  46607  stoweidlem29  46608  stoweidlem31  46610  stoweidlem35  46614  stoweidlem48  46627  stoweidlem51  46630  stoweidlem52  46631  stoweidlem53  46632  stoweidlem54  46633  stoweidlem56  46635  stoweidlem57  46636  stoweidlem59  46638  stoweidlem60  46639  stoweidlem62  46641  wallispilem3  46646  stirlinglem13  46665  fourierdlem31  46717  fourierdlem39  46725  fourierdlem68  46753  fourierdlem71  46756  fourierdlem73  46758  fourierdlem77  46762  fourierdlem83  46768  fourierdlem87  46772  fourierdlem94  46779  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  fourierdlem113  46798  salexct  46913  subsaliuncl  46937  sge0lefi  46977  sge0isum  47006  sge0reuzb  47027  iundjiun  47039  voliunsge0lem  47051  meaiuninc3v  47063  ovnsubaddlem2  47150  hoiqssbllem3  47203  vonioo  47261  vonicc  47264  preimageiingt  47299  preimaleiinlt  47300  issmfle  47324  issmfgt  47335  issmfge  47349  smflimlem2  47351  smfsupmpt  47394  smfinflem  47396  smfinfmpt  47398  smfliminflem  47409  fsupdm  47421  finfdm  47425  ffnafv  47770  iccelpart  48044  sprsymrelfo  48108  mogoldbb  48412  sbgoldbo  48414  iunord  50302  setrec1lem2  50314  pgind  50343  aacllem  50427