Theorem nfra1 3259

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  3273  r19.12  3285  nfra2  3347  ralcom2  3348  2reu1  3857  nfss  3936  2reu4lem  4481  iuneqconst  4963  nfii1  4989  mpteq12f  5187  reusv1  5347  reusv2lem1  5348  reusv2lem2  5349  reusv2lem3  5350  ralxfrALT  5365  fvmptss  6962  fompt  7072  ffnfv  7073  riota5f  7354  mpoeq123  7441  tfinds  7816  zfrep6  7913  frrlem4  8245  tfr3  8344  tz7.48-1  8388  tz7.49  8390  naddsuc2  8642  nfixp1  8868  nneneq  9147  scottex  9814  dfac2b  10060  infpssrlem4  10235  hsmexlem2  10356  hsmexlem4  10358  domtriomlem  10371  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  zorn2lem5  10429  konigthlem  10497  eltsk2g  10680  dedekind  11313  dedekindle  11314  lble  12111  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  fsuppmapnn0fiubex  13933  prodeq2ii  15853  fprodle  15938  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2  16586  mreiincl  17533  mreexexd  17589  catpropd  17650  acsmapd  18495  gsummatr01lem4  22578  cpmatmcllem  22638  alexsubALTlem3  23969  isucn2  24199  nosupbnd1  27659  noinfbnd1  27674  mptelee  28875  chirred  32374  opreu2reuALT  32456  foresf1o  32483  abrexss  32491  iinabrex  32548  aciunf1lem  32636  nn0min  32795  fprodex01  32800  isarchiofld  33168  elrspunidl  33392  reff  33822  locfinreflem  33823  cmpcref  33833  zarcmplem  33864  esumcl  34013  measvunilem  34195  measvunilem0  34196  measvuni  34197  voliune  34212  volfiniune  34213  omssubadd  34284  bnj1366  34812  bnj1379  34813  bnj571  34889  bnj1039  34954  bnj1128  34973  bnj1204  34995  bnj1279  35001  bnj1307  35006  bnj1388  35016  bnj1398  35017  bnj1444  35026  bnj1489  35039  bnj1525  35052  dfon2lem3  35766  domalom  37385  ralssiun  37388  fvineqsneu  37392  fvineqsneq  37393  heicant  37642  cover2  37702  upixp  37716  indexdom  37721  filbcmb  37727  riotasvd  38942  riotasv2d  38943  riotasv2s  38944  glbconxN  39365  pmapglbx  39756  pmapglb2xN  39759  cdleme26ee  40347  cdlemefr29exN  40389  cdlemefs32sn1aw  40401  cdleme43fsv1snlem  40407  cdleme41sn3a  40420  cdleme32d  40431  cdleme32f  40433  cdleme40m  40454  cdleme40n  40455  cdlemk36  40900  cdlemk38  40902  cdlemkid  40923  cdlemk19x  40930  cdlemk11t  40933  mzpexpmpt  42726  nadd1suc  43374  gneispace  44116  mnuprdlem4  44257  ssralv2  44514  tratrb  44519  modelaxrep  44964  fnchoice  45016  rfcnnnub  45023  uzwo4  45040  ralimralim  45068  suprnmpt  45161  choicefi  45187  axccdom  45209  axccd  45216  rnmptlb  45230  rnmptbddlem  45231  rnmptbd2lem  45235  rnmptbdlem  45242  upbdrech  45296  ssfiunibd  45300  iuneqfzuzlem  45323  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  49658  setrec1lem2  49670  pgind  49699  aacllem  49783