Theorem nfra1 3253

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784  df-ral 3045

This theorem is referenced by:  hbra1  3266  r19.12  3278  nfra2  3339  ralcom2  3340  2reu1  3849  nfss  3928  2reu4lem  4473  iuneqconst  4953  nfii1  4979  mpteq12f  5177  reusv1  5336  reusv2lem1  5337  reusv2lem2  5338  reusv2lem3  5339  ralxfrALT  5354  fvmptss  6942  fompt  7052  ffnfv  7053  riota5f  7334  mpoeq123  7421  tfinds  7793  zfrep6  7890  frrlem4  8222  tfr3  8321  tz7.48-1  8365  tz7.49  8367  naddsuc2  8619  nfixp1  8845  nneneq  9120  scottex  9781  dfac2b  10025  infpssrlem4  10200  hsmexlem2  10321  hsmexlem4  10323  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  zorn2lem5  10394  konigthlem  10462  eltsk2g  10645  dedekind  11279  dedekindle  11280  lble  12077  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  22543  cpmatmcllem  22603  alexsubALTlem3  23934  isucn2  24164  nosupbnd1  27624  noinfbnd1  27639  mptelee  28840  chirred  32339  opreu2reuALT  32421  foresf1o  32448  abrexss  32456  iinabrex  32513  aciunf1lem  32606  nn0min  32766  fprodex01  32771  isarchiofld  33142  elrspunidl  33366  reff  33812  locfinreflem  33813  cmpcref  33823  zarcmplem  33854  esumcl  34003  measvunilem  34185  measvunilem0  34186  measvuni  34187  voliune  34202  volfiniune  34203  omssubadd  34274  bnj1366  34802  bnj1379  34803  bnj571  34879  bnj1039  34944  bnj1128  34963  bnj1204  34985  bnj1279  34991  bnj1307  34996  bnj1388  35006  bnj1398  35007  bnj1444  35016  bnj1489  35029  bnj1525  35042  dfon2lem3  35769  domalom  37388  ralssiun  37391  fvineqsneu  37395  fvineqsneq  37396  heicant  37645  cover2  37705  upixp  37719  indexdom  37724  filbcmb  37730  riotasvd  38945  riotasv2d  38946  riotasv2s  38947  glbconxN  39367  pmapglbx  39758  pmapglb2xN  39761  cdleme26ee  40349  cdlemefr29exN  40391  cdlemefs32sn1aw  40403  cdleme43fsv1snlem  40409  cdleme41sn3a  40422  cdleme32d  40433  cdleme32f  40435  cdleme40m  40456  cdleme40n  40457  cdlemk36  40902  cdlemk38  40904  cdlemkid  40925  cdlemk19x  40932  cdlemk11t  40935  mzpexpmpt  42728  nadd1suc  43375  gneispace  44117  mnuprdlem4  44258  ssralv2  44515  tratrb  44520  modelaxrep  44965  fnchoice  45017  rfcnnnub  45024  uzwo4  45041  ralimralim  45069  suprnmpt  45162  choicefi  45188  axccdom  45210  axccd  45217  rnmptlb  45231  rnmptbddlem  45232  rnmptbd2lem  45236  rnmptbdlem  45243  upbdrech  45297  ssfiunibd  45301  iuneqfzuzlem  45324  infxrunb2  45357  xrralrecnnle  45372  supxrunb3  45388  supxrleubrnmpt  45395  unb2ltle  45404  rexabslelem  45407  allbutfiinf  45409  suprleubrnmpt  45411  uzub  45420  infxrgelbrnmpt  45443  cvgcaule  45480  mccl  45589  climsuse  45599  mullimc  45607  islptre  45610  mullimcf  45614  limcrecl  45620  islpcn  45630  limsupre  45632  limcleqr  45635  addlimc  45639  0ellimcdiv  45640  limclner  45642  climinf2lem  45697  limsupubuz  45704  climinf3  45707  limsupmnflem  45711  limsupmnfuzlem  45717  limsupre3uzlem  45726  climisp  45737  climrescn  45739  climxrrelem  45740  climxrre  45741  xlimmnfv  45825  xlimpnfv  45829  climxlim2lem  45836  cncfioobd  45888  stoweidlem16  46007  stoweidlem28  46019  stoweidlem29  46020  stoweidlem31  46022  stoweidlem35  46026  stoweidlem48  46039  stoweidlem51  46042  stoweidlem52  46043  stoweidlem53  46044  stoweidlem54  46045  stoweidlem56  46047  stoweidlem57  46048  stoweidlem59  46050  stoweidlem60  46051  stoweidlem62  46053  wallispilem3  46058  stirlinglem13  46077  fourierdlem31  46129  fourierdlem39  46137  fourierdlem68  46165  fourierdlem71  46168  fourierdlem73  46170  fourierdlem77  46174  fourierdlem83  46180  fourierdlem87  46184  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  salexct  46325  subsaliuncl  46349  sge0lefi  46389  sge0isum  46418  sge0reuzb  46439  iundjiun  46451  voliunsge0lem  46463  meaiuninc3v  46475  ovnsubaddlem2  46562  hoiqssbllem3  46615  vonioo  46673  vonicc  46676  preimageiingt  46711  preimaleiinlt  46712  issmfle  46736  issmfgt  46747  issmfge  46761  smflimlem2  46763  smfsupmpt  46806  smfinflem  46808  smfinfmpt  46810  smfliminflem  46821  fsupdm  46833  finfdm  46837  ffnafv  47165  iccelpart  47427  sprsymrelfo  47491  mogoldbb  47779  sbgoldbo  47781  iunord  49671  setrec1lem2  49683  pgind  49712  aacllem  49796