Theorem nfra1 3262

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 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 2157	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1855	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  hbra1  3275  r19.12  3287  nfra2  3348  ralcom2  3349  2reu1  3849  nfss  3928  2reu4lem  4478  iuneqconst  4960  nfii1  4986  mpteq12f  5185  reusv1  5346  reusv2lem1  5347  reusv2lem2  5348  reusv2lem3  5349  ralxfrALT  5364  fvmptss  6964  fompt  7074  ffnfv  7075  riota5f  7355  mpoeq123  7442  tfinds  7814  zfrep6OLD  7911  frrlem4  8243  tfr3  8342  tz7.48-1  8386  tz7.49  8388  naddsuc2  8641  nfixp1  8870  nneneq  9144  scottex  9811  dfac2b  10055  infpssrlem4  10230  hsmexlem2  10351  hsmexlem4  10353  domtriomlem  10366  axdc3lem2  10375  axdc3lem4  10377  axdc4lem  10379  zorn2lem5  10424  konigthlem  10493  eltsk2g  10676  dedekind  11310  dedekindle  11311  lble  12108  fsuppmapnn0fiublem  13927  fsuppmapnn0fiub  13928  fsuppmapnn0fiubex  13929  prodeq2ii  15848  fprodle  15933  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2  16581  mreiincl  17529  mreexexd  17585  catpropd  17646  acsmapd  18491  gsummatr01lem4  22619  cpmatmcllem  22679  alexsubALTlem3  24010  isucn2  24239  nosupbnd1  27699  noinfbnd1  27714  bdaypw2n0bndlem  28476  mpteleeOLD  28986  chirred  32489  opreu2reuALT  32569  foresf1o  32597  abrexss  32605  iinabrex  32662  aciunf1lem  32758  nn0min  32918  fprodex01  32923  isarchiofld  33299  elrspunidl  33527  vieta  33763  reff  34023  locfinreflem  34024  cmpcref  34034  zarcmplem  34065  esumcl  34214  measvunilem  34396  measvunilem0  34397  measvuni  34398  voliune  34413  volfiniune  34414  omssubadd  34484  bnj1366  35011  bnj1379  35012  bnj571  35088  bnj1039  35153  bnj1128  35172  bnj1204  35194  bnj1279  35200  bnj1307  35205  bnj1388  35215  bnj1398  35216  bnj1444  35225  bnj1489  35238  bnj1525  35251  dfon2lem3  36005  domalom  37686  ralssiun  37689  fvineqsneu  37693  fvineqsneq  37694  heicant  37935  cover2  37995  upixp  38009  indexdom  38014  filbcmb  38020  riotasvd  39361  riotasv2d  39362  riotasv2s  39363  glbconxN  39783  pmapglbx  40174  pmapglb2xN  40177  cdleme26ee  40765  cdlemefr29exN  40807  cdlemefs32sn1aw  40819  cdleme43fsv1snlem  40825  cdleme41sn3a  40838  cdleme32d  40849  cdleme32f  40851  cdleme40m  40872  cdleme40n  40873  cdlemk36  41318  cdlemk38  41320  cdlemkid  41341  cdlemk19x  41348  cdlemk11t  41351  mzpexpmpt  43131  nadd1suc  43778  gneispace  44519  mnuprdlem4  44660  ssralv2  44916  tratrb  44921  modelaxrep  45366  fnchoice  45418  rfcnnnub  45425  uzwo4  45442  ralimralim  45470  suprnmpt  45562  choicefi  45587  axccdom  45609  axccd  45616  rnmptlb  45630  rnmptbddlem  45631  rnmptbd2lem  45635  rnmptbdlem  45642  upbdrech  45696  ssfiunibd  45700  iuneqfzuzlem  45722  infxrunb2  45755  xrralrecnnle  45770  supxrunb3  45786  supxrleubrnmpt  45793  unb2ltle  45802  rexabslelem  45805  allbutfiinf  45807  suprleubrnmpt  45809  uzub  45818  infxrgelbrnmpt  45841  cvgcaule  45878  mccl  45987  climsuse  45997  mullimc  46005  islptre  46008  mullimcf  46012  limcrecl  46018  islpcn  46026  limsupre  46028  limcleqr  46031  addlimc  46035  0ellimcdiv  46036  limclner  46038  climinf2lem  46093  limsupubuz  46100  climinf3  46103  limsupmnflem  46107  limsupmnfuzlem  46113  limsupre3uzlem  46122  climisp  46133  climrescn  46135  climxrrelem  46136  climxrre  46137  xlimmnfv  46221  xlimpnfv  46225  climxlim2lem  46232  cncfioobd  46284  stoweidlem16  46403  stoweidlem28  46415  stoweidlem29  46416  stoweidlem31  46418  stoweidlem35  46422  stoweidlem48  46435  stoweidlem51  46438  stoweidlem52  46439  stoweidlem53  46440  stoweidlem54  46441  stoweidlem56  46443  stoweidlem57  46444  stoweidlem59  46446  stoweidlem60  46447  stoweidlem62  46449  wallispilem3  46454  stirlinglem13  46473  fourierdlem31  46525  fourierdlem39  46533  fourierdlem68  46561  fourierdlem71  46564  fourierdlem73  46566  fourierdlem77  46570  fourierdlem83  46576  fourierdlem87  46580  fourierdlem94  46587  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem113  46606  salexct  46721  subsaliuncl  46745  sge0lefi  46785  sge0isum  46814  sge0reuzb  46835  iundjiun  46847  voliunsge0lem  46859  meaiuninc3v  46871  ovnsubaddlem2  46958  hoiqssbllem3  47011  vonioo  47069  vonicc  47072  preimageiingt  47107  preimaleiinlt  47108  issmfle  47132  issmfgt  47143  issmfge  47157  smflimlem2  47159  smfsupmpt  47202  smfinflem  47204  smfinfmpt  47206  smfliminflem  47217  fsupdm  47229  finfdm  47233  ffnafv  47560  iccelpart  47822  sprsymrelfo  47886  mogoldbb  48174  sbgoldbo  48176  iunord  50064  setrec1lem2  50076  pgind  50105  aacllem  50189