Theorem nfra1 3183

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

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

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 3111

This theorem is referenced by:  hbra1  3184  nfra2w  3191  nfra2  3192  ralrexbidOLD  3282  r19.12  3283  ralcom2  3316  2reu1  3826  nfss  3907  rspn0OLD  4267  ralidm  4413  2reu4lem  4423  iuneqconst  4892  nfii1  4916  dfiun2g  4917  dfiun2gOLD  4918  mpteq12f  5113  reusv1  5263  reusv2lem1  5264  reusv2lem2  5265  reusv2lem3  5266  ralxfrALT  5281  fvmptss  6757  ffnfv  6859  riota5f  7121  mpoeq123  7205  tfinds  7554  peano5  7585  zfrep6  7638  wfrlem4  7941  tfr3  8018  tz7.48-1  8062  tz7.49  8064  nfixp1  8465  nneneq  8684  scottex  9298  dfac2b  9541  infpssrlem4  9717  hsmexlem2  9838  hsmexlem4  9840  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  zorn2lem5  9911  konigthlem  9979  eltsk2g  10162  dedekind  10792  dedekindle  10793  lble  11580  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  fsuppmapnn0fiubex  13355  prodeq2ii  15259  fprodle  15342  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  mreiincl  16859  mreexexd  16911  catpropd  16971  acsmapd  17780  gsummatr01lem4  21263  cpmatmcllem  21323  alexsubALTlem3  22654  isucn2  22885  mptelee  26689  chirred  30178  opreu2reuALT  30247  foresf1o  30273  abrexss  30280  iinabrex  30332  aciunf1lem  30425  nn0min  30562  fprodex01  30567  isarchiofld  30941  elrspunidl  31014  reff  31192  locfinreflem  31193  cmpcref  31203  zarcmplem  31234  esumcl  31399  measvunilem  31581  measvunilem0  31582  measvuni  31583  voliune  31598  volfiniune  31599  omssubadd  31668  bnj1366  32211  bnj1379  32212  bnj571  32288  bnj1039  32353  bnj1128  32372  bnj1204  32394  bnj1279  32400  bnj1307  32405  bnj1388  32415  bnj1398  32416  bnj1444  32425  bnj1489  32438  bnj1525  32451  dfon2lem3  33143  trpredmintr  33183  frrlem4  33239  nosupbnd1  33327  domalom  34821  ralssiun  34824  fvineqsneu  34828  fvineqsneq  34829  heicant  35092  cover2  35152  upixp  35167  indexdom  35172  filbcmb  35178  riotasvd  36252  riotasv2d  36253  riotasv2s  36254  glbconxN  36674  pmapglbx  37065  pmapglb2xN  37068  cdleme26ee  37656  cdlemefr29exN  37698  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme41sn3a  37729  cdleme32d  37740  cdleme32f  37742  cdleme40m  37763  cdleme40n  37764  cdlemk36  38209  cdlemk38  38211  cdlemkid  38232  cdlemk19x  38239  cdlemk11t  38242  mzpexpmpt  39686  gneispace  40837  mnuprdlem4  40983  ssralv2  41237  tratrb  41242  fnchoice  41658  rfcnnnub  41665  uzwo4  41687  ralimralim  41717  ralimda  41774  suprnmpt  41798  fompt  41819  choicefi  41829  axccdom  41853  axccd  41861  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  rnmptbdlem  41893  upbdrech  41937  ssfiunibd  41941  iuneqfzuzlem  41966  infxrunb2  42000  xrralrecnnle  42017  supxrunb3  42036  supxrleubrnmpt  42043  unb2ltle  42052  rexabslelem  42055  allbutfiinf  42057  suprleubrnmpt  42059  uzub  42068  infxrgelbrnmpt  42093  mccl  42240  climsuse  42250  mullimc  42258  islptre  42261  mullimcf  42265  limcrecl  42271  islpcn  42281  limsupre  42283  limcleqr  42286  addlimc  42290  0ellimcdiv  42291  limclner  42293  climinf2lem  42348  limsupubuz  42355  climinf3  42358  limsupmnflem  42362  limsupmnfuzlem  42368  limsupre3uzlem  42377  climisp  42388  climrescn  42390  climxrrelem  42391  climxrre  42392  xlimmnfv  42476  xlimpnfv  42480  climxlim2lem  42487  cncfioobd  42539  stoweidlem16  42658  stoweidlem28  42670  stoweidlem29  42671  stoweidlem31  42673  stoweidlem35  42677  stoweidlem48  42690  stoweidlem51  42693  stoweidlem52  42694  stoweidlem53  42695  stoweidlem54  42696  stoweidlem56  42698  stoweidlem57  42699  stoweidlem59  42701  stoweidlem60  42702  stoweidlem62  42704  wallispilem3  42709  stirlinglem13  42728  fourierdlem31  42780  fourierdlem39  42788  fourierdlem68  42816  fourierdlem71  42819  fourierdlem73  42821  fourierdlem77  42825  fourierdlem83  42831  fourierdlem87  42835  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  salexct  42974  subsaliuncl  42998  sge0lefi  43037  sge0isum  43066  sge0reuzb  43087  iundjiun  43099  voliunsge0lem  43111  meaiuninc3v  43123  ovnsubaddlem2  43210  hoiqssbllem3  43263  vonioo  43321  vonicc  43324  preimageiingt  43355  preimaleiinlt  43356  issmfle  43379  issmfgt  43390  issmfge  43403  smflimlem2  43405  smfsupmpt  43446  smfinflem  43448  smfinfmpt  43450  smfliminflem  43461  ffnafv  43727  iccelpart  43950  sprsymrelfo  44014  mogoldbb  44303  sbgoldbo  44305  iunord  45206  setrec1lem2  45218  aacllem  45329