Theorem nfra1 3147

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

Syntax hints:   → wi 4  ∀wal 1536  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2142

This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786  df-ral 3075

This theorem is referenced by:  hbra1  3148  nfra2w  3155  nfra2  3156  ralrexbidOLD  3247  r19.12  3248  ralcom2  3281  ralimda  3408  2reu1  3805  nfss  3886  rspn0OLD  4254  ralidmOLD  4411  2reu4lem  4421  iuneqconst  4897  nfii1  4921  dfiun2g  4922  dfiun2gOLD  4923  mpteq12f  5118  reusv1  5269  reusv2lem1  5270  reusv2lem2  5271  reusv2lem3  5272  ralxfrALT  5287  fvmptss  6775  ffnfv  6878  riota5f  7141  mpoeq123  7225  tfinds  7578  peano5  7609  zfrep6  7665  wfrlem4  7973  tfr3  8050  tz7.48-1  8094  tz7.49  8096  nfixp1  8505  nneneq  8727  scottex  9352  dfac2b  9595  infpssrlem4  9771  hsmexlem2  9892  hsmexlem4  9894  domtriomlem  9907  axdc3lem2  9916  axdc3lem4  9918  axdc4lem  9920  zorn2lem5  9965  konigthlem  10033  eltsk2g  10216  dedekind  10846  dedekindle  10847  lble  11634  fsuppmapnn0fiublem  13412  fsuppmapnn0fiub  13413  fsuppmapnn0fiubex  13414  prodeq2ii  15320  fprodle  15403  lcmfunsnlem1  16038  lcmfunsnlem2lem1  16039  lcmfunsnlem2  16041  mreiincl  16930  mreexexd  16982  catpropd  17042  acsmapd  17859  gsummatr01lem4  21363  cpmatmcllem  21423  alexsubALTlem3  22754  isucn2  22985  mptelee  26793  chirred  30282  opreu2reuALT  30351  foresf1o  30377  abrexss  30384  iinabrex  30435  aciunf1lem  30527  nn0min  30662  fprodex01  30667  isarchiofld  31046  elrspunidl  31131  reff  31314  locfinreflem  31315  cmpcref  31325  zarcmplem  31356  esumcl  31521  measvunilem  31703  measvunilem0  31704  measvuni  31705  voliune  31720  volfiniune  31721  omssubadd  31790  bnj1366  32333  bnj1379  32334  bnj571  32410  bnj1039  32475  bnj1128  32494  bnj1204  32516  bnj1279  32522  bnj1307  32527  bnj1388  32537  bnj1398  32538  bnj1444  32547  bnj1489  32560  bnj1525  32573  dfon2lem3  33281  trpredmintr  33321  frrlem4  33392  nosupbnd1  33506  noinfbnd1  33521  no3indslem  33689  domalom  35127  ralssiun  35130  fvineqsneu  35134  fvineqsneq  35135  heicant  35398  cover2  35458  upixp  35473  indexdom  35478  filbcmb  35484  riotasvd  36558  riotasv2d  36559  riotasv2s  36560  glbconxN  36980  pmapglbx  37371  pmapglb2xN  37374  cdleme26ee  37962  cdlemefr29exN  38004  cdlemefs32sn1aw  38016  cdleme43fsv1snlem  38022  cdleme41sn3a  38035  cdleme32d  38046  cdleme32f  38048  cdleme40m  38069  cdleme40n  38070  cdlemk36  38515  cdlemk38  38517  cdlemkid  38538  cdlemk19x  38545  cdlemk11t  38548  mzpexpmpt  40087  gneispace  41238  mnuprdlem4  41384  ssralv2  41638  tratrb  41643  fnchoice  42059  rfcnnnub  42066  uzwo4  42088  ralimralim  42118  suprnmpt  42197  fompt  42217  choicefi  42227  axccdom  42249  axccd  42257  rnmptlb  42276  rnmptbddlem  42277  rnmptbd2lem  42282  rnmptbdlem  42289  upbdrech  42333  ssfiunibd  42337  iuneqfzuzlem  42362  infxrunb2  42396  xrralrecnnle  42413  supxrunb3  42430  supxrleubrnmpt  42437  unb2ltle  42446  rexabslelem  42449  allbutfiinf  42451  suprleubrnmpt  42453  uzub  42462  infxrgelbrnmpt  42487  mccl  42634  climsuse  42644  mullimc  42652  islptre  42655  mullimcf  42659  limcrecl  42665  islpcn  42675  limsupre  42677  limcleqr  42680  addlimc  42684  0ellimcdiv  42685  limclner  42687  climinf2lem  42742  limsupubuz  42749  climinf3  42752  limsupmnflem  42756  limsupmnfuzlem  42762  limsupre3uzlem  42771  climisp  42782  climrescn  42784  climxrrelem  42785  climxrre  42786  xlimmnfv  42870  xlimpnfv  42874  climxlim2lem  42881  cncfioobd  42933  stoweidlem16  43052  stoweidlem28  43064  stoweidlem29  43065  stoweidlem31  43067  stoweidlem35  43071  stoweidlem48  43084  stoweidlem51  43087  stoweidlem52  43088  stoweidlem53  43089  stoweidlem54  43090  stoweidlem56  43092  stoweidlem57  43093  stoweidlem59  43095  stoweidlem60  43096  stoweidlem62  43098  wallispilem3  43103  stirlinglem13  43122  fourierdlem31  43174  fourierdlem39  43182  fourierdlem68  43210  fourierdlem71  43213  fourierdlem73  43215  fourierdlem77  43219  fourierdlem83  43225  fourierdlem87  43229  fourierdlem94  43236  fourierdlem103  43245  fourierdlem104  43246  fourierdlem112  43254  fourierdlem113  43255  salexct  43368  subsaliuncl  43392  sge0lefi  43431  sge0isum  43460  sge0reuzb  43481  iundjiun  43493  voliunsge0lem  43505  meaiuninc3v  43517  ovnsubaddlem2  43604  hoiqssbllem3  43657  vonioo  43715  vonicc  43718  preimageiingt  43749  preimaleiinlt  43750  issmfle  43773  issmfgt  43784  issmfge  43797  smflimlem2  43799  smfsupmpt  43840  smfinflem  43842  smfinfmpt  43844  smfliminflem  43855  ffnafv  44123  iccelpart  44346  sprsymrelfo  44410  mogoldbb  44698  sbgoldbo  44700  iunord  45670  setrec1lem2  45682  aacllem  45793