Theorem nfra1 3258

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3049

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 2146

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

This theorem is referenced by:  hbra1  3271  r19.12  3283  nfra2  3344  ralcom2  3345  2reu1  3845  nfss  3924  2reu4lem  4474  iuneqconst  4956  nfii1  4982  mpteq12f  5181  reusv1  5340  reusv2lem1  5341  reusv2lem2  5342  reusv2lem3  5343  ralxfrALT  5358  fvmptss  6951  fompt  7061  ffnfv  7062  riota5f  7341  mpoeq123  7428  tfinds  7800  zfrep6  7897  frrlem4  8229  tfr3  8328  tz7.48-1  8372  tz7.49  8374  naddsuc2  8627  nfixp1  8854  nneneq  9128  scottex  9795  dfac2b  10039  infpssrlem4  10214  hsmexlem2  10335  hsmexlem4  10337  domtriomlem  10350  axdc3lem2  10359  axdc3lem4  10361  axdc4lem  10363  zorn2lem5  10408  konigthlem  10477  eltsk2g  10660  dedekind  11294  dedekindle  11295  lble  12092  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  fsuppmapnn0fiubex  13913  prodeq2ii  15832  fprodle  15917  lcmfunsnlem1  16562  lcmfunsnlem2lem1  16563  lcmfunsnlem2  16565  mreiincl  17513  mreexexd  17569  catpropd  17630  acsmapd  18475  gsummatr01lem4  22600  cpmatmcllem  22660  alexsubALTlem3  23991  isucn2  24220  nosupbnd1  27680  noinfbnd1  27695  bdaypw2n0s  28420  mpteleeOLD  28917  chirred  32419  opreu2reuALT  32500  foresf1o  32528  abrexss  32536  iinabrex  32593  aciunf1lem  32689  nn0min  32850  fprodex01  32855  isarchiofld  33230  elrspunidl  33458  vieta  33685  reff  33945  locfinreflem  33946  cmpcref  33956  zarcmplem  33987  esumcl  34136  measvunilem  34318  measvunilem0  34319  measvuni  34320  voliune  34335  volfiniune  34336  omssubadd  34406  bnj1366  34934  bnj1379  34935  bnj571  35011  bnj1039  35076  bnj1128  35095  bnj1204  35117  bnj1279  35123  bnj1307  35128  bnj1388  35138  bnj1398  35139  bnj1444  35148  bnj1489  35161  bnj1525  35174  dfon2lem3  35926  domalom  37548  ralssiun  37551  fvineqsneu  37555  fvineqsneq  37556  heicant  37795  cover2  37855  upixp  37869  indexdom  37874  filbcmb  37880  riotasvd  39155  riotasv2d  39156  riotasv2s  39157  glbconxN  39577  pmapglbx  39968  pmapglb2xN  39971  cdleme26ee  40559  cdlemefr29exN  40601  cdlemefs32sn1aw  40613  cdleme43fsv1snlem  40619  cdleme41sn3a  40632  cdleme32d  40643  cdleme32f  40645  cdleme40m  40666  cdleme40n  40667  cdlemk36  41112  cdlemk38  41114  cdlemkid  41135  cdlemk19x  41142  cdlemk11t  41145  mzpexpmpt  42929  nadd1suc  43576  gneispace  44317  mnuprdlem4  44458  ssralv2  44714  tratrb  44719  modelaxrep  45164  fnchoice  45216  rfcnnnub  45223  uzwo4  45240  ralimralim  45268  suprnmpt  45360  choicefi  45386  axccdom  45408  axccd  45415  rnmptlb  45429  rnmptbddlem  45430  rnmptbd2lem  45434  rnmptbdlem  45441  upbdrech  45495  ssfiunibd  45499  iuneqfzuzlem  45521  infxrunb2  45554  xrralrecnnle  45569  supxrunb3  45585  supxrleubrnmpt  45592  unb2ltle  45601  rexabslelem  45604  allbutfiinf  45606  suprleubrnmpt  45608  uzub  45617  infxrgelbrnmpt  45640  cvgcaule  45677  mccl  45786  climsuse  45796  mullimc  45804  islptre  45807  mullimcf  45811  limcrecl  45817  islpcn  45825  limsupre  45827  limcleqr  45830  addlimc  45834  0ellimcdiv  45835  limclner  45837  climinf2lem  45892  limsupubuz  45899  climinf3  45902  limsupmnflem  45906  limsupmnfuzlem  45912  limsupre3uzlem  45921  climisp  45932  climrescn  45934  climxrrelem  45935  climxrre  45936  xlimmnfv  46020  xlimpnfv  46024  climxlim2lem  46031  cncfioobd  46083  stoweidlem16  46202  stoweidlem28  46214  stoweidlem29  46215  stoweidlem31  46217  stoweidlem35  46221  stoweidlem48  46234  stoweidlem51  46237  stoweidlem52  46238  stoweidlem53  46239  stoweidlem54  46240  stoweidlem56  46242  stoweidlem57  46243  stoweidlem59  46245  stoweidlem60  46246  stoweidlem62  46248  wallispilem3  46253  stirlinglem13  46272  fourierdlem31  46324  fourierdlem39  46332  fourierdlem68  46360  fourierdlem71  46363  fourierdlem73  46365  fourierdlem77  46369  fourierdlem83  46375  fourierdlem87  46379  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  fourierdlem113  46405  salexct  46520  subsaliuncl  46544  sge0lefi  46584  sge0isum  46613  sge0reuzb  46634  iundjiun  46646  voliunsge0lem  46658  meaiuninc3v  46670  ovnsubaddlem2  46757  hoiqssbllem3  46810  vonioo  46868  vonicc  46871  preimageiingt  46906  preimaleiinlt  46907  issmfle  46931  issmfgt  46942  issmfge  46956  smflimlem2  46958  smfsupmpt  47001  smfinflem  47003  smfinfmpt  47005  smfliminflem  47016  fsupdm  47028  finfdm  47032  ffnafv  47359  iccelpart  47621  sprsymrelfo  47685  mogoldbb  47973  sbgoldbo  47975  iunord  49863  setrec1lem2  49875  pgind  49904  aacllem  49988