Theorem nfra1 3281

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

Syntax hints:   → wi 4  ∀wal 1534  Ⅎwnf 1779   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-10 2138

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1776  df-nf 1780  df-ral 3059

This theorem is referenced by:  hbra1  3298  r19.12  3311  r19.12OLD  3312  nfra2  3373  ralcom2  3374  2reu1  3905  nfss  3987  2reu4lem  4527  iuneqconst  5007  nfii1  5033  dfiun2gOLD  5035  mpteq12f  5235  reusv1  5402  reusv2lem1  5403  reusv2lem2  5404  reusv2lem3  5405  ralxfrALT  5420  fvmptss  7027  fompt  7137  ffnfv  7138  riota5f  7415  mpoeq123  7504  tfinds  7880  zfrep6  7977  frrlem4  8312  wfrlem4OLD  8350  tfr3  8437  tz7.48-1  8481  tz7.49  8483  naddsuc2  8737  nfixp1  8956  nneneq  9243  nneneqOLD  9255  scottex  9922  dfac2b  10168  infpssrlem4  10343  hsmexlem2  10464  hsmexlem4  10466  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  zorn2lem5  10537  konigthlem  10605  eltsk2g  10788  dedekind  11421  dedekindle  11422  lble  12217  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  fsuppmapnn0fiubex  14029  prodeq2ii  15943  fprodle  16028  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  mreiincl  17640  mreexexd  17692  catpropd  17753  acsmapd  18611  gsummatr01lem4  22679  cpmatmcllem  22739  alexsubALTlem3  24072  isucn2  24303  nosupbnd1  27773  noinfbnd1  27788  mptelee  28924  chirred  32423  opreu2reuALT  32504  foresf1o  32531  abrexss  32539  iinabrex  32588  aciunf1lem  32678  nn0min  32826  fprodex01  32831  isarchiofld  33326  elrspunidl  33435  reff  33799  locfinreflem  33800  cmpcref  33810  zarcmplem  33841  esumcl  34010  measvunilem  34192  measvunilem0  34193  measvuni  34194  voliune  34209  volfiniune  34210  omssubadd  34281  bnj1366  34821  bnj1379  34822  bnj571  34898  bnj1039  34963  bnj1128  34982  bnj1204  35004  bnj1279  35010  bnj1307  35015  bnj1388  35025  bnj1398  35026  bnj1444  35035  bnj1489  35048  bnj1525  35061  dfon2lem3  35766  domalom  37386  ralssiun  37389  fvineqsneu  37393  fvineqsneq  37394  heicant  37641  cover2  37701  upixp  37715  indexdom  37720  filbcmb  37726  riotasvd  38937  riotasv2d  38938  riotasv2s  38939  glbconxN  39360  pmapglbx  39751  pmapglb2xN  39754  cdleme26ee  40342  cdlemefr29exN  40384  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32d  40426  cdleme32f  40428  cdleme40m  40449  cdleme40n  40450  cdlemk36  40895  cdlemk38  40897  cdlemkid  40918  cdlemk19x  40925  cdlemk11t  40928  mzpexpmpt  42732  nadd1suc  43381  gneispace  44123  mnuprdlem4  44270  ssralv2  44528  tratrb  44533  modelaxrep  44945  fnchoice  44966  rfcnnnub  44973  uzwo4  44992  ralimralim  45020  suprnmpt  45116  choicefi  45142  axccdom  45164  axccd  45171  rnmptlb  45187  rnmptbddlem  45188  rnmptbd2lem  45192  rnmptbdlem  45199  upbdrech  45255  ssfiunibd  45259  iuneqfzuzlem  45283  infxrunb2  45317  xrralrecnnle  45332  supxrunb3  45348  supxrleubrnmpt  45355  unb2ltle  45364  rexabslelem  45367  allbutfiinf  45369  suprleubrnmpt  45371  uzub  45380  infxrgelbrnmpt  45403  cvgcaule  45441  mccl  45553  climsuse  45563  mullimc  45571  islptre  45574  mullimcf  45578  limcrecl  45584  islpcn  45594  limsupre  45596  limcleqr  45599  addlimc  45603  0ellimcdiv  45604  limclner  45606  climinf2lem  45661  limsupubuz  45668  climinf3  45671  limsupmnflem  45675  limsupmnfuzlem  45681  limsupre3uzlem  45690  climisp  45701  climrescn  45703  climxrrelem  45704  climxrre  45705  xlimmnfv  45789  xlimpnfv  45793  climxlim2lem  45800  cncfioobd  45852  stoweidlem16  45971  stoweidlem28  45983  stoweidlem29  45984  stoweidlem31  45986  stoweidlem35  45990  stoweidlem48  46003  stoweidlem51  46006  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  stoweidlem56  46011  stoweidlem57  46012  stoweidlem59  46014  stoweidlem60  46015  stoweidlem62  46017  wallispilem3  46022  stirlinglem13  46041  fourierdlem31  46093  fourierdlem39  46101  fourierdlem68  46129  fourierdlem71  46132  fourierdlem73  46134  fourierdlem77  46138  fourierdlem83  46144  fourierdlem87  46148  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  salexct  46289  subsaliuncl  46313  sge0lefi  46353  sge0isum  46382  sge0reuzb  46403  iundjiun  46415  voliunsge0lem  46427  meaiuninc3v  46439  ovnsubaddlem2  46526  hoiqssbllem3  46579  vonioo  46637  vonicc  46640  preimageiingt  46675  preimaleiinlt  46676  issmfle  46700  issmfgt  46711  issmfge  46725  smflimlem2  46727  smfsupmpt  46770  smfinflem  46772  smfinfmpt  46774  smfliminflem  46785  fsupdm  46797  finfdm  46801  ffnafv  47120  iccelpart  47357  sprsymrelfo  47421  mogoldbb  47709  sbgoldbo  47711  iunord  48906  setrec1lem2  48918  pgind  48947  aacllem  49031