Theorem nfra1 3261

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

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

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 3052

This theorem is referenced by:  hbra1  3274  r19.12  3286  nfra2  3338  ralcom2  3339  2reu1  3835  nfss  3914  2reu4lem  4463  iuneqconst  4945  nfii1  4971  mpteq12f  5170  reusv1  5339  reusv2lem1  5340  reusv2lem2  5341  reusv2lem3  5342  ralxfrALT  5357  fvmptss  6960  fompt  7070  ffnfv  7071  riota5f  7352  mpoeq123  7439  tfinds  7811  zfrep6OLD  7908  frrlem4  8239  tfr3  8338  tz7.48-1  8382  tz7.49  8384  naddsuc2  8637  nfixp1  8866  nneneq  9140  scottex  9809  dfac2b  10053  infpssrlem4  10228  hsmexlem2  10349  hsmexlem4  10351  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  zorn2lem5  10422  konigthlem  10491  eltsk2g  10674  dedekind  11309  dedekindle  11310  lble  12108  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiubex  13954  prodeq2ii  15876  fprodle  15961  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  mreiincl  17558  mreexexd  17614  catpropd  17675  acsmapd  18520  gsummatr01lem4  22623  cpmatmcllem  22683  alexsubALTlem3  24014  isucn2  24243  nosupbnd1  27678  noinfbnd1  27693  bdaypw2n0bndlem  28455  mpteleeOLD  28964  chirred  32466  opreu2reuALT  32546  foresf1o  32574  abrexss  32582  iinabrex  32639  aciunf1lem  32735  nn0min  32894  fprodex01  32898  isarchiofld  33260  elrspunidl  33488  vieta  33724  reff  33983  locfinreflem  33984  cmpcref  33994  zarcmplem  34025  esumcl  34174  measvunilem  34356  measvunilem0  34357  measvuni  34358  voliune  34373  volfiniune  34374  omssubadd  34444  bnj1366  34971  bnj1379  34972  bnj571  35048  bnj1039  35113  bnj1128  35132  bnj1204  35154  bnj1279  35160  bnj1307  35165  bnj1388  35175  bnj1398  35176  bnj1444  35185  bnj1489  35198  bnj1525  35211  dfon2lem3  35965  domalom  37720  ralssiun  37723  fvineqsneu  37727  fvineqsneq  37728  heicant  37976  cover2  38036  upixp  38050  indexdom  38055  filbcmb  38061  riotasvd  39402  riotasv2d  39403  riotasv2s  39404  glbconxN  39824  pmapglbx  40215  pmapglb2xN  40218  cdleme26ee  40806  cdlemefr29exN  40848  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32d  40890  cdleme32f  40892  cdleme40m  40913  cdleme40n  40914  cdlemk36  41359  cdlemk38  41361  cdlemkid  41382  cdlemk19x  41389  cdlemk11t  41392  mzpexpmpt  43177  nadd1suc  43820  gneispace  44561  mnuprdlem4  44702  ssralv2  44958  tratrb  44963  modelaxrep  45408  fnchoice  45460  rfcnnnub  45467  uzwo4  45484  ralimralim  45512  suprnmpt  45604  choicefi  45629  axccdom  45651  axccd  45658  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  rnmptbdlem  45684  upbdrech  45738  ssfiunibd  45742  iuneqfzuzlem  45764  infxrunb2  45797  xrralrecnnle  45812  supxrunb3  45828  supxrleubrnmpt  45834  unb2ltle  45843  rexabslelem  45846  allbutfiinf  45848  suprleubrnmpt  45850  uzub  45859  infxrgelbrnmpt  45882  cvgcaule  45919  mccl  46028  climsuse  46038  mullimc  46046  islptre  46049  mullimcf  46053  limcrecl  46059  islpcn  46067  limsupre  46069  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  climinf2lem  46134  limsupubuz  46141  climinf3  46144  limsupmnflem  46148  limsupmnfuzlem  46154  limsupre3uzlem  46163  climisp  46174  climrescn  46176  climxrrelem  46177  climxrre  46178  xlimmnfv  46262  xlimpnfv  46266  climxlim2lem  46273  cncfioobd  46325  stoweidlem16  46444  stoweidlem28  46456  stoweidlem29  46457  stoweidlem31  46459  stoweidlem35  46463  stoweidlem48  46476  stoweidlem51  46479  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem56  46484  stoweidlem57  46485  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  wallispilem3  46495  stirlinglem13  46514  fourierdlem31  46566  fourierdlem39  46574  fourierdlem68  46602  fourierdlem71  46605  fourierdlem73  46607  fourierdlem77  46611  fourierdlem83  46617  fourierdlem87  46621  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  salexct  46762  subsaliuncl  46786  sge0lefi  46826  sge0isum  46855  sge0reuzb  46876  iundjiun  46888  voliunsge0lem  46900  meaiuninc3v  46912  ovnsubaddlem2  46999  hoiqssbllem3  47052  vonioo  47110  vonicc  47113  preimageiingt  47148  preimaleiinlt  47149  issmfle  47173  issmfgt  47184  issmfge  47198  smflimlem2  47200  smfsupmpt  47243  smfinflem  47245  smfinfmpt  47247  smfliminflem  47258  fsupdm  47270  finfdm  47274  ffnafv  47619  iccelpart  47893  sprsymrelfo  47957  mogoldbb  48261  sbgoldbo  48263  iunord  50151  setrec1lem2  50163  pgind  50192  aacllem  50276