Theorem nfra1 3142

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-10 2139

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

This theorem is referenced by:  hbra1  3143  nfra2wOLDOLD  3153  nfra2  3154  r19.12  3252  r19.12OLD  3253  ralcom2  3288  ralimda  3421  2reu1  3826  nfss  3909  rspn0OLD  4284  ralidmOLD  4443  2reu4lem  4453  iuneqconst  4932  nfii1  4956  dfiun2g  4957  mpteq12f  5158  reusv1  5315  reusv2lem1  5316  reusv2lem2  5317  reusv2lem3  5318  ralxfrALT  5333  fvmptss  6869  ffnfv  6974  riota5f  7241  mpoeq123  7325  tfinds  7681  peano5OLD  7715  zfrep6  7771  frrlem4  8076  wfrlem4OLD  8114  tfr3  8201  tz7.48-1  8244  tz7.49  8246  nfixp1  8664  nneneq  8896  trpredmintr  9409  scottex  9574  dfac2b  9817  infpssrlem4  9993  hsmexlem2  10114  hsmexlem4  10116  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  zorn2lem5  10187  konigthlem  10255  eltsk2g  10438  dedekind  11068  dedekindle  11069  lble  11857  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  fsuppmapnn0fiubex  13640  prodeq2ii  15551  fprodle  15634  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  mreiincl  17222  mreexexd  17274  catpropd  17335  acsmapd  18187  gsummatr01lem4  21715  cpmatmcllem  21775  alexsubALTlem3  23108  isucn2  23339  mptelee  27166  chirred  30658  opreu2reuALT  30726  foresf1o  30751  abrexss  30758  iinabrex  30809  aciunf1lem  30901  nn0min  31036  fprodex01  31041  isarchiofld  31418  elrspunidl  31508  reff  31691  locfinreflem  31692  cmpcref  31702  zarcmplem  31733  esumcl  31898  measvunilem  32080  measvunilem0  32081  measvuni  32082  voliune  32097  volfiniune  32098  omssubadd  32167  bnj1366  32709  bnj1379  32710  bnj571  32786  bnj1039  32851  bnj1128  32870  bnj1204  32892  bnj1279  32898  bnj1307  32903  bnj1388  32913  bnj1398  32914  bnj1444  32923  bnj1489  32936  bnj1525  32949  dfon2lem3  33667  nosupbnd1  33844  noinfbnd1  33859  domalom  35502  ralssiun  35505  fvineqsneu  35509  fvineqsneq  35510  heicant  35739  cover2  35799  upixp  35814  indexdom  35819  filbcmb  35825  riotasvd  36897  riotasv2d  36898  riotasv2s  36899  glbconxN  37319  pmapglbx  37710  pmapglb2xN  37713  cdleme26ee  38301  cdlemefr29exN  38343  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32d  38385  cdleme32f  38387  cdleme40m  38408  cdleme40n  38409  cdlemk36  38854  cdlemk38  38856  cdlemkid  38877  cdlemk19x  38884  cdlemk11t  38887  mzpexpmpt  40483  gneispace  41633  mnuprdlem4  41782  ssralv2  42040  tratrb  42045  fnchoice  42461  rfcnnnub  42468  uzwo4  42490  ralimralim  42520  suprnmpt  42599  fompt  42619  choicefi  42629  axccdom  42651  axccd  42657  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  rnmptbdlem  42690  upbdrech  42734  ssfiunibd  42738  iuneqfzuzlem  42763  infxrunb2  42797  xrralrecnnle  42812  supxrunb3  42829  supxrleubrnmpt  42836  unb2ltle  42845  rexabslelem  42848  allbutfiinf  42850  suprleubrnmpt  42852  uzub  42861  infxrgelbrnmpt  42884  mccl  43029  climsuse  43039  mullimc  43047  islptre  43050  mullimcf  43054  limcrecl  43060  islpcn  43070  limsupre  43072  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  limclner  43082  climinf2lem  43137  limsupubuz  43144  climinf3  43147  limsupmnflem  43151  limsupmnfuzlem  43157  limsupre3uzlem  43166  climisp  43177  climrescn  43179  climxrrelem  43180  climxrre  43181  xlimmnfv  43265  xlimpnfv  43269  climxlim2lem  43276  cncfioobd  43328  stoweidlem16  43447  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem35  43466  stoweidlem48  43479  stoweidlem51  43482  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem56  43487  stoweidlem57  43488  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  wallispilem3  43498  stirlinglem13  43517  fourierdlem31  43569  fourierdlem39  43577  fourierdlem68  43605  fourierdlem71  43608  fourierdlem73  43610  fourierdlem77  43614  fourierdlem83  43620  fourierdlem87  43624  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  salexct  43763  subsaliuncl  43787  sge0lefi  43826  sge0isum  43855  sge0reuzb  43876  iundjiun  43888  voliunsge0lem  43900  meaiuninc3v  43912  ovnsubaddlem2  43999  hoiqssbllem3  44052  vonioo  44110  vonicc  44113  preimageiingt  44144  preimaleiinlt  44145  issmfle  44168  issmfgt  44179  issmfge  44192  smflimlem2  44194  smfsupmpt  44235  smfinflem  44237  smfinfmpt  44239  smfliminflem  44250  ffnafv  44550  iccelpart  44773  sprsymrelfo  44837  mogoldbb  45125  sbgoldbo  45127  iunord  46268  setrec1lem2  46280  aacllem  46391