Theorem nfra1 3263

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

Syntax hints:   → wi 4  ∀wal 1545  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791  df-ral 3054

This theorem is referenced by:  hbra1  3276  r19.12  3288  nfra2  3340  ralcom2  3341  2reu1  3829  nfss  3908  2reu4lem  4452  iuneqconst  4934  nfii1  4959  mpteq12f  5158  reusv1  5327  reusv2lem1  5328  reusv2lem2  5329  reusv2lem3  5330  ralxfrALT  5345  fvmptss  6949  fompt  7060  ffnfv  7061  riota5f  7342  mpoeq123  7429  tfinds  7801  zfrep6OLD  7898  frrlem4  8230  tfr3  8329  tz7.48-1  8373  tz7.49  8375  naddsuc2  8628  nfixp1  8857  nneneq  9131  scottex  9801  dfac2b  10045  infpssrlem4  10220  hsmexlem2  10341  hsmexlem4  10343  domtriomlem  10356  axdc3lem2  10365  axdc3lem4  10367  axdc4lem  10369  zorn2lem5  10414  konigthlem  10483  eltsk2g  10666  dedekind  11301  dedekindle  11302  lble  12100  fsuppmapnn0fiublem  13944  fsuppmapnn0fiub  13945  fsuppmapnn0fiubex  13946  prodeq2ii  15868  fprodle  15953  lcmfunsnlem1  16598  lcmfunsnlem2lem1  16599  lcmfunsnlem2  16601  mreiincl  17550  mreexexd  17606  catpropd  17667  acsmapd  18512  gsummatr01lem4  22642  cpmatmcllem  22702  alexsubALTlem3  24033  isucn2  24262  nosupbnd1  27697  noinfbnd1  27712  bdaypw2n0bndlem  28474  mpteleeOLD  28983  chirred  32485  opreu2reuALT  32565  foresf1o  32593  abrexss  32601  iinabrex  32659  aciunf1lem  32755  nn0min  32914  fprodex01  32918  isarchiofld  33281  elrspunidl  33512  vieta  33773  reff  34032  locfinreflem  34033  cmpcref  34043  zarcmplem  34074  esumcl  34223  measvunilem  34405  measvunilem0  34406  measvuni  34407  voliune  34422  volfiniune  34423  omssubadd  34493  bnj1366  35020  bnj1379  35021  bnj571  35097  bnj1039  35162  bnj1128  35181  bnj1204  35203  bnj1279  35209  bnj1307  35214  bnj1388  35224  bnj1398  35225  bnj1444  35234  bnj1489  35247  bnj1525  35260  dfon2lem3  36020  domalom  37775  ralssiun  37778  fvineqsneu  37782  fvineqsneq  37783  heicant  38031  cover2  38091  upixp  38105  indexdom  38110  filbcmb  38116  riotasvd  39457  riotasv2d  39458  riotasv2s  39459  glbconxN  39879  pmapglbx  40270  pmapglb2xN  40273  cdleme26ee  40861  cdlemefr29exN  40903  cdlemefs32sn1aw  40915  cdleme43fsv1snlem  40921  cdleme41sn3a  40934  cdleme32d  40945  cdleme32f  40947  cdleme40m  40968  cdleme40n  40969  cdlemk36  41414  cdlemk38  41416  cdlemkid  41437  cdlemk19x  41444  cdlemk11t  41447  mzpexpmpt  43203  nadd1suc  43846  gneispace  44587  mnuprdlem4  44728  ssralv2  44984  tratrb  44989  modelaxrep  45434  fnchoice  45486  rfcnnnub  45493  uzwo4  45510  ralimralim  45538  suprnmpt  45629  choicefi  45654  axccdom  45675  axccd  45681  rnmptlb  45695  rnmptbddlem  45696  rnmptbd2lem  45700  rnmptbdlem  45707  upbdrech  45761  ssfiunibd  45765  iuneqfzuzlem  45787  infxrunb2  45820  xrralrecnnle  45835  supxrunb3  45851  supxrleubrnmpt  45857  unb2ltle  45866  rexabslelem  45869  allbutfiinf  45871  suprleubrnmpt  45873  uzub  45882  infxrgelbrnmpt  45905  cvgcaule  45942  mccl  46051  climsuse  46061  mullimc  46069  islptre  46072  mullimcf  46076  limcrecl  46082  islpcn  46090  limsupre  46092  limcleqr  46095  addlimc  46099  0ellimcdiv  46100  limclner  46102  climinf2lem  46157  limsupubuz  46164  climinf3  46167  limsupmnflem  46171  limsupmnfuzlem  46177  limsupre3uzlem  46186  climisp  46197  climrescn  46199  climxrrelem  46200  climxrre  46201  xlimmnfv  46285  xlimpnfv  46289  climxlim2lem  46296  cncfioobd  46348  stoweidlem16  46467  stoweidlem28  46479  stoweidlem29  46480  stoweidlem31  46482  stoweidlem35  46486  stoweidlem48  46499  stoweidlem51  46502  stoweidlem52  46503  stoweidlem53  46504  stoweidlem54  46505  stoweidlem56  46507  stoweidlem57  46508  stoweidlem59  46510  stoweidlem60  46511  stoweidlem62  46513  wallispilem3  46518  stirlinglem13  46537  fourierdlem31  46589  fourierdlem39  46597  fourierdlem68  46625  fourierdlem71  46628  fourierdlem73  46630  fourierdlem77  46634  fourierdlem83  46640  fourierdlem87  46644  fourierdlem94  46651  fourierdlem103  46660  fourierdlem104  46661  fourierdlem112  46669  fourierdlem113  46670  salexct  46785  subsaliuncl  46809  sge0lefi  46849  sge0isum  46878  sge0reuzb  46899  iundjiun  46911  voliunsge0lem  46923  meaiuninc3v  46935  ovnsubaddlem2  47022  hoiqssbllem3  47075  vonioo  47133  vonicc  47136  preimageiingt  47171  preimaleiinlt  47172  issmfle  47196  issmfgt  47207  issmfge  47221  smflimlem2  47223  smfsupmpt  47266  smfinflem  47268  smfinfmpt  47270  smfliminflem  47281  fsupdm  47293  finfdm  47297  ffnafv  47642  iccelpart  47916  sprsymrelfo  47980  mogoldbb  48284  sbgoldbo  48286  iunord  50174  setrec1lem2  50186  pgind  50215  aacllem  50299