Theorem nfra1 3279

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1783   ∈ wcel 2104  ∀wral 3059

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 2135

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1780  df-nf 1784  df-ral 3060

This theorem is referenced by:  hbra1  3296  r19.12  3309  r19.12OLD  3310  nfra2wOLDOLD  3317  nfra2  3370  ralcom2  3371  2reu1  3892  nfss  3975  rspn0OLD  4354  ralidmOLD  4516  2reu4lem  4526  iuneqconst  5009  nfii1  5033  dfiun2gOLD  5035  mpteq12f  5237  reusv1  5396  reusv2lem1  5397  reusv2lem2  5398  reusv2lem3  5399  ralxfrALT  5414  fvmptss  7011  fompt  7120  ffnfv  7121  riota5f  7398  mpoeq123  7485  tfinds  7853  peano5OLD  7889  zfrep6  7945  frrlem4  8278  wfrlem4OLD  8316  tfr3  8403  tz7.48-1  8447  tz7.49  8449  nfixp1  8916  nneneq  9213  nneneqOLD  9225  scottex  9884  dfac2b  10129  infpssrlem4  10305  hsmexlem2  10426  hsmexlem4  10428  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  zorn2lem5  10499  konigthlem  10567  eltsk2g  10750  dedekind  11383  dedekindle  11384  lble  12172  fsuppmapnn0fiublem  13961  fsuppmapnn0fiub  13962  fsuppmapnn0fiubex  13963  prodeq2ii  15863  fprodle  15946  lcmfunsnlem1  16580  lcmfunsnlem2lem1  16581  lcmfunsnlem2  16583  mreiincl  17546  mreexexd  17598  catpropd  17659  acsmapd  18513  gsummatr01lem4  22382  cpmatmcllem  22442  alexsubALTlem3  23775  isucn2  24006  nosupbnd1  27451  noinfbnd1  27466  mptelee  28418  chirred  31913  opreu2reuALT  31982  foresf1o  32007  abrexss  32014  iinabrex  32065  aciunf1lem  32152  nn0min  32291  fprodex01  32296  isarchiofld  32703  elrspunidl  32818  reff  33115  locfinreflem  33116  cmpcref  33126  zarcmplem  33157  esumcl  33324  measvunilem  33506  measvunilem0  33507  measvuni  33508  voliune  33523  volfiniune  33524  omssubadd  33595  bnj1366  34136  bnj1379  34137  bnj571  34213  bnj1039  34278  bnj1128  34297  bnj1204  34319  bnj1279  34325  bnj1307  34330  bnj1388  34340  bnj1398  34341  bnj1444  34350  bnj1489  34363  bnj1525  34376  dfon2lem3  35059  domalom  36590  ralssiun  36593  fvineqsneu  36597  fvineqsneq  36598  heicant  36828  cover2  36888  upixp  36902  indexdom  36907  filbcmb  36913  riotasvd  38131  riotasv2d  38132  riotasv2s  38133  glbconxN  38554  pmapglbx  38945  pmapglb2xN  38948  cdleme26ee  39536  cdlemefr29exN  39578  cdlemefs32sn1aw  39590  cdleme43fsv1snlem  39596  cdleme41sn3a  39609  cdleme32d  39620  cdleme32f  39622  cdleme40m  39643  cdleme40n  39644  cdlemk36  40089  cdlemk38  40091  cdlemkid  40112  cdlemk19x  40119  cdlemk11t  40122  mzpexpmpt  41787  nadd1suc  42446  naddsuc2  42447  gneispace  43189  mnuprdlem4  43338  ssralv2  43596  tratrb  43601  fnchoice  44017  rfcnnnub  44024  uzwo4  44043  ralimralim  44073  suprnmpt  44173  choicefi  44199  axccdom  44221  axccd  44228  rnmptlb  44247  rnmptbddlem  44248  rnmptbd2lem  44252  rnmptbdlem  44259  upbdrech  44315  ssfiunibd  44319  iuneqfzuzlem  44344  infxrunb2  44378  xrralrecnnle  44393  supxrunb3  44409  supxrleubrnmpt  44416  unb2ltle  44425  rexabslelem  44428  allbutfiinf  44430  suprleubrnmpt  44432  uzub  44441  infxrgelbrnmpt  44464  cvgcaule  44502  mccl  44614  climsuse  44624  mullimc  44632  islptre  44635  mullimcf  44639  limcrecl  44645  islpcn  44655  limsupre  44657  limcleqr  44660  addlimc  44664  0ellimcdiv  44665  limclner  44667  climinf2lem  44722  limsupubuz  44729  climinf3  44732  limsupmnflem  44736  limsupmnfuzlem  44742  limsupre3uzlem  44751  climisp  44762  climrescn  44764  climxrrelem  44765  climxrre  44766  xlimmnfv  44850  xlimpnfv  44854  climxlim2lem  44861  cncfioobd  44913  stoweidlem16  45032  stoweidlem28  45044  stoweidlem29  45045  stoweidlem31  45047  stoweidlem35  45051  stoweidlem48  45064  stoweidlem51  45067  stoweidlem52  45068  stoweidlem53  45069  stoweidlem54  45070  stoweidlem56  45072  stoweidlem57  45073  stoweidlem59  45075  stoweidlem60  45076  stoweidlem62  45078  wallispilem3  45083  stirlinglem13  45102  fourierdlem31  45154  fourierdlem39  45162  fourierdlem68  45190  fourierdlem71  45193  fourierdlem73  45195  fourierdlem77  45199  fourierdlem83  45205  fourierdlem87  45209  fourierdlem94  45216  fourierdlem103  45225  fourierdlem104  45226  fourierdlem112  45234  fourierdlem113  45235  salexct  45350  subsaliuncl  45374  sge0lefi  45414  sge0isum  45443  sge0reuzb  45464  iundjiun  45476  voliunsge0lem  45488  meaiuninc3v  45500  ovnsubaddlem2  45587  hoiqssbllem3  45640  vonioo  45698  vonicc  45701  preimageiingt  45736  preimaleiinlt  45737  issmfle  45761  issmfgt  45772  issmfge  45786  smflimlem2  45788  smfsupmpt  45831  smfinflem  45833  smfinfmpt  45835  smfliminflem  45846  fsupdm  45858  finfdm  45862  ffnafv  46179  iccelpart  46401  sprsymrelfo  46465  mogoldbb  46753  sbgoldbo  46755  iunord  47810  setrec1lem2  47822  pgind  47851  aacllem  47937