Theorem nfra1 3282

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787  df-ral 3063

This theorem is referenced by:  hbra1  3299  r19.12  3312  r19.12OLD  3313  nfra2wOLDOLD  3320  nfra2  3373  ralcom2  3374  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  ffnfv  7118  riota5f  7394  mpoeq123  7481  tfinds  7849  peano5OLD  7885  zfrep6  7941  frrlem4  8274  wfrlem4OLD  8312  tfr3  8399  tz7.48-1  8443  tz7.49  8445  nfixp1  8912  nneneq  9209  nneneqOLD  9221  scottex  9880  dfac2b  10125  infpssrlem4  10301  hsmexlem2  10422  hsmexlem4  10424  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  zorn2lem5  10495  konigthlem  10563  eltsk2g  10746  dedekind  11377  dedekindle  11378  lble  12166  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  prodeq2ii  15857  fprodle  15940  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  mreiincl  17540  mreexexd  17592  catpropd  17653  acsmapd  18507  gsummatr01lem4  22160  cpmatmcllem  22220  alexsubALTlem3  23553  isucn2  23784  nosupbnd1  27217  noinfbnd1  27232  mptelee  28153  chirred  31648  opreu2reuALT  31717  foresf1o  31742  abrexss  31749  iinabrex  31800  aciunf1lem  31887  nn0min  32026  fprodex01  32031  isarchiofld  32435  elrspunidl  32546  reff  32819  locfinreflem  32820  cmpcref  32830  zarcmplem  32861  esumcl  33028  measvunilem  33210  measvunilem0  33211  measvuni  33212  voliune  33227  volfiniune  33228  omssubadd  33299  bnj1366  33840  bnj1379  33841  bnj571  33917  bnj1039  33982  bnj1128  34001  bnj1204  34023  bnj1279  34029  bnj1307  34034  bnj1388  34044  bnj1398  34045  bnj1444  34054  bnj1489  34067  bnj1525  34080  dfon2lem3  34757  domalom  36285  ralssiun  36288  fvineqsneu  36292  fvineqsneq  36293  heicant  36523  cover2  36583  upixp  36597  indexdom  36602  filbcmb  36608  riotasvd  37826  riotasv2d  37827  riotasv2s  37828  glbconxN  38249  pmapglbx  38640  pmapglb2xN  38643  cdleme26ee  39231  cdlemefr29exN  39273  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme41sn3a  39304  cdleme32d  39315  cdleme32f  39317  cdleme40m  39338  cdleme40n  39339  cdlemk36  39784  cdlemk38  39786  cdlemkid  39807  cdlemk19x  39814  cdlemk11t  39817  mzpexpmpt  41483  nadd1suc  42142  naddsuc2  42143  gneispace  42885  mnuprdlem4  43034  ssralv2  43292  tratrb  43297  fnchoice  43713  rfcnnnub  43720  uzwo4  43740  ralimralim  43770  suprnmpt  43870  fompt  43890  choicefi  43899  axccdom  43921  axccd  43928  rnmptlb  43947  rnmptbddlem  43948  rnmptbd2lem  43952  rnmptbdlem  43959  upbdrech  44015  ssfiunibd  44019  iuneqfzuzlem  44044  infxrunb2  44078  xrralrecnnle  44093  supxrunb3  44109  supxrleubrnmpt  44116  unb2ltle  44125  rexabslelem  44128  allbutfiinf  44130  suprleubrnmpt  44132  uzub  44141  infxrgelbrnmpt  44164  cvgcaule  44202  mccl  44314  climsuse  44324  mullimc  44332  islptre  44335  mullimcf  44339  limcrecl  44345  islpcn  44355  limsupre  44357  limcleqr  44360  addlimc  44364  0ellimcdiv  44365  limclner  44367  climinf2lem  44422  limsupubuz  44429  climinf3  44432  limsupmnflem  44436  limsupmnfuzlem  44442  limsupre3uzlem  44451  climisp  44462  climrescn  44464  climxrrelem  44465  climxrre  44466  xlimmnfv  44550  xlimpnfv  44554  climxlim2lem  44561  cncfioobd  44613  stoweidlem16  44732  stoweidlem28  44744  stoweidlem29  44745  stoweidlem31  44747  stoweidlem35  44751  stoweidlem48  44764  stoweidlem51  44767  stoweidlem52  44768  stoweidlem53  44769  stoweidlem54  44770  stoweidlem56  44772  stoweidlem57  44773  stoweidlem59  44775  stoweidlem60  44776  stoweidlem62  44778  wallispilem3  44783  stirlinglem13  44802  fourierdlem31  44854  fourierdlem39  44862  fourierdlem68  44890  fourierdlem71  44893  fourierdlem73  44895  fourierdlem77  44899  fourierdlem83  44905  fourierdlem87  44909  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem113  44935  salexct  45050  subsaliuncl  45074  sge0lefi  45114  sge0isum  45143  sge0reuzb  45164  iundjiun  45176  voliunsge0lem  45188  meaiuninc3v  45200  ovnsubaddlem2  45287  hoiqssbllem3  45340  vonioo  45398  vonicc  45401  preimageiingt  45436  preimaleiinlt  45437  issmfle  45461  issmfgt  45472  issmfge  45486  smflimlem2  45488  smfsupmpt  45531  smfinflem  45533  smfinfmpt  45535  smfliminflem  45546  fsupdm  45558  finfdm  45562  ffnafv  45879  iccelpart  46101  sprsymrelfo  46165  mogoldbb  46453  sbgoldbo  46455  iunord  47721  setrec1lem2  47733  pgind  47762  aacllem  47848