Theorem nfra1 3256

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047

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-10 2144

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785  df-ral 3048

This theorem is referenced by:  hbra1  3269  r19.12  3281  nfra2  3342  ralcom2  3343  2reu1  3843  nfss  3922  2reu4lem  4469  iuneqconst  4951  nfii1  4977  mpteq12f  5174  reusv1  5333  reusv2lem1  5334  reusv2lem2  5335  reusv2lem3  5336  ralxfrALT  5351  fvmptss  6941  fompt  7051  ffnfv  7052  riota5f  7331  mpoeq123  7418  tfinds  7790  zfrep6  7887  frrlem4  8219  tfr3  8318  tz7.48-1  8362  tz7.49  8364  naddsuc2  8616  nfixp1  8842  nneneq  9115  scottex  9778  dfac2b  10022  infpssrlem4  10197  hsmexlem2  10318  hsmexlem4  10320  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  zorn2lem5  10391  konigthlem  10459  eltsk2g  10642  dedekind  11276  dedekindle  11277  lble  12074  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fsuppmapnn0fiubex  13899  prodeq2ii  15818  fprodle  15903  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  mreiincl  17498  mreexexd  17554  catpropd  17615  acsmapd  18460  gsummatr01lem4  22573  cpmatmcllem  22633  alexsubALTlem3  23964  isucn2  24193  nosupbnd1  27653  noinfbnd1  27668  mptelee  28873  chirred  32375  opreu2reuALT  32456  foresf1o  32484  abrexss  32492  iinabrex  32549  aciunf1lem  32644  nn0min  32803  fprodex01  32808  isarchiofld  33168  elrspunidl  33393  reff  33852  locfinreflem  33853  cmpcref  33863  zarcmplem  33894  esumcl  34043  measvunilem  34225  measvunilem0  34226  measvuni  34227  voliune  34242  volfiniune  34243  omssubadd  34313  bnj1366  34841  bnj1379  34842  bnj571  34918  bnj1039  34983  bnj1128  35002  bnj1204  35024  bnj1279  35030  bnj1307  35035  bnj1388  35045  bnj1398  35046  bnj1444  35055  bnj1489  35068  bnj1525  35081  dfon2lem3  35827  domalom  37448  ralssiun  37451  fvineqsneu  37455  fvineqsneq  37456  heicant  37705  cover2  37765  upixp  37779  indexdom  37784  filbcmb  37790  riotasvd  39065  riotasv2d  39066  riotasv2s  39067  glbconxN  39487  pmapglbx  39878  pmapglb2xN  39881  cdleme26ee  40469  cdlemefr29exN  40511  cdlemefs32sn1aw  40523  cdleme43fsv1snlem  40529  cdleme41sn3a  40542  cdleme32d  40553  cdleme32f  40555  cdleme40m  40576  cdleme40n  40577  cdlemk36  41022  cdlemk38  41024  cdlemkid  41045  cdlemk19x  41052  cdlemk11t  41055  mzpexpmpt  42848  nadd1suc  43495  gneispace  44237  mnuprdlem4  44378  ssralv2  44634  tratrb  44639  modelaxrep  45084  fnchoice  45136  rfcnnnub  45143  uzwo4  45160  ralimralim  45188  suprnmpt  45281  choicefi  45307  axccdom  45329  axccd  45336  rnmptlb  45350  rnmptbddlem  45351  rnmptbd2lem  45355  rnmptbdlem  45362  upbdrech  45416  ssfiunibd  45420  iuneqfzuzlem  45443  infxrunb2  45476  xrralrecnnle  45491  supxrunb3  45507  supxrleubrnmpt  45514  unb2ltle  45523  rexabslelem  45526  allbutfiinf  45528  suprleubrnmpt  45530  uzub  45539  infxrgelbrnmpt  45562  cvgcaule  45599  mccl  45708  climsuse  45718  mullimc  45726  islptre  45729  mullimcf  45733  limcrecl  45739  islpcn  45747  limsupre  45749  limcleqr  45752  addlimc  45756  0ellimcdiv  45757  limclner  45759  climinf2lem  45814  limsupubuz  45821  climinf3  45824  limsupmnflem  45828  limsupmnfuzlem  45834  limsupre3uzlem  45843  climisp  45854  climrescn  45856  climxrrelem  45857  climxrre  45858  xlimmnfv  45942  xlimpnfv  45946  climxlim2lem  45953  cncfioobd  46005  stoweidlem16  46124  stoweidlem28  46136  stoweidlem29  46137  stoweidlem31  46139  stoweidlem35  46143  stoweidlem48  46156  stoweidlem51  46159  stoweidlem52  46160  stoweidlem53  46161  stoweidlem54  46162  stoweidlem56  46164  stoweidlem57  46165  stoweidlem59  46167  stoweidlem60  46168  stoweidlem62  46170  wallispilem3  46175  stirlinglem13  46194  fourierdlem31  46246  fourierdlem39  46254  fourierdlem68  46282  fourierdlem71  46285  fourierdlem73  46287  fourierdlem77  46291  fourierdlem83  46297  fourierdlem87  46301  fourierdlem94  46308  fourierdlem103  46317  fourierdlem104  46318  fourierdlem112  46326  fourierdlem113  46327  salexct  46442  subsaliuncl  46466  sge0lefi  46506  sge0isum  46535  sge0reuzb  46556  iundjiun  46568  voliunsge0lem  46580  meaiuninc3v  46592  ovnsubaddlem2  46679  hoiqssbllem3  46732  vonioo  46790  vonicc  46793  preimageiingt  46828  preimaleiinlt  46829  issmfle  46853  issmfgt  46864  issmfge  46878  smflimlem2  46880  smfsupmpt  46923  smfinflem  46925  smfinfmpt  46927  smfliminflem  46938  fsupdm  46950  finfdm  46954  ffnafv  47281  iccelpart  47543  sprsymrelfo  47607  mogoldbb  47895  sbgoldbo  47897  iunord  49787  setrec1lem2  49799  pgind  49828  aacllem  49912