Theorem nfra1 3289

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1813   ∈ wcel 2143  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-10 2176

This proof depends on definitions:  df-bi 210  df-or 861  df-ex 1810  df-nf 1814  df-ral 3080

This theorem is used by:  hbra1  3302  r19.12  3314  nfra2  3365  ralcom2  3366  2reu1  3851  nfss  3930  2reu4lem  4484  iuneqconst  4968  nfii1  4993  mpteq12f  5196  reusv1  5368  reusv2lem1  5369  reusv2lem2  5370  reusv2lem3  5371  ralxfrALT  5386  fvmptss  7002  fompt  7113  ffnfv  7114  riota5f  7395  mpoeq123  7482  tfinds  7852  zfrep6OLD  7948  frrlem4  8282  tfr3  8382  tz7.48-1  8426  tz7.49  8428  naddsuc2  8684  nfixp1  8912  nneneq  9186  scottexOLD  9859  dfac2b  10119  infpssrlem4  10294  hsmexlem2  10415  hsmexlem4  10417  domtriomlem  10430  axdc3lem2  10439  axdc3lem4  10441  axdc4lem  10443  zorn2lem5  10488  konigthlem  10557  eltsk2g  10740  dedekind  11377  dedekindle  11378  lble  12171  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  fsuppmapnn0fiubex  14033  prodeq2ii  15970  fprodle  16055  lcmfunsnlem1  16699  lcmfunsnlem2lem1  16700  lcmfunsnlem2  16702  mreiincl  17652  mreexexd  17708  catpropd  17769  acsmapd  18614  gsummatr01lem4  22824  cpmatmcllem  22884  alexsubALTlem3  24215  isucn2  24444  nosupbnd1  27887  noinfbnd1  27902  bdaypw2n0bndlem  28665  mpteleeOLD  29254  chirred  32756  opreu2reuALT  32832  foresf1o  32859  abrexss  32867  iinabrex  32923  aciunf1lem  33016  nn0min  33174  fprodex01  33178  isarchiofld  33528  elrspunidl  33745  vieta  33979  reff  34238  locfinreflem  34239  cmpcref  34249  zarcmplem  34280  esumcl  34429  measvunilem  34611  measvunilem0  34612  measvuni  34613  voliune  34628  volfiniune  34629  omssubadd  34699  bnj1366  35226  bnj1379  35227  bnj571  35303  bnj1039  35368  bnj1128  35387  bnj1204  35409  bnj1279  35415  bnj1307  35420  bnj1388  35430  bnj1398  35431  bnj1444  35440  bnj1489  35453  bnj1525  35466  dfon2lem3  36283  domalom  38078  ralssiun  38081  fvineqsneu  38085  fvineqsneq  38086  heicant  38334  cover2  38394  upixp  38408  indexdom  38413  filbcmb  38419  riotasvd  39758  riotasv2d  39759  riotasv2s  39760  glbconxN  40180  pmapglbx  40571  pmapglb2xN  40574  cdleme26ee  41162  cdlemefr29exN  41204  cdlemefs32sn1aw  41216  cdleme43fsv1snlem  41222  cdleme41sn3a  41235  cdleme32d  41246  cdleme32f  41248  cdleme40m  41269  cdleme40n  41270  cdlemk36  41715  cdlemk38  41717  cdlemkid  41738  cdlemk19x  41745  cdlemk11t  41748  mzpexpmpt  43504  nadd1suc  44147  gneispace  44888  mnuprdlem4  45013  ssralv2  45268  tratrb  45273  modelaxrep  45718  fnchoice  45777  rfcnnnub  45784  uzwo4  45801  ralimralim  45829  suprnmpt  45920  choicefi  45945  axccdom  45966  axccd  45972  rnmptlb  45986  rnmptbddlem  45987  rnmptbd2lem  45991  rnmptbdlem  45998  upbdrech  46052  ssfiunibd  46056  iuneqfzuzlem  46078  infxrunb2  46111  xrralrecnnle  46126  supxrunb3  46142  supxrleubrnmpt  46148  unb2ltle  46157  rexabslelem  46160  allbutfiinf  46162  suprleubrnmpt  46164  uzub  46173  infxrgelbrnmpt  46196  cvgcaule  46233  mccl  46342  climsuse  46352  mullimc  46360  islptre  46363  mullimcf  46367  limcrecl  46373  islpcn  46381  limsupre  46383  limcleqr  46386  addlimc  46390  0ellimcdiv  46391  limclner  46393  climinf2lem  46448  limsupubuz  46455  climinf3  46458  limsupmnflem  46462  limsupmnfuzlem  46468  limsupre3uzlem  46477  climisp  46488  climrescn  46490  climxrrelem  46491  climxrre  46492  xlimmnfv  46576  xlimpnfv  46580  climxlim2lem  46587  cncfioobd  46639  stoweidlem16  46758  stoweidlem28  46770  stoweidlem29  46771  stoweidlem31  46773  stoweidlem35  46777  stoweidlem48  46790  stoweidlem51  46793  stoweidlem52  46794  stoweidlem53  46795  stoweidlem54  46796  stoweidlem56  46798  stoweidlem57  46799  stoweidlem59  46801  stoweidlem60  46802  stoweidlem62  46804  wallispilem3  46809  stirlinglem13  46828  fourierdlem31  46880  fourierdlem39  46888  fourierdlem68  46916  fourierdlem71  46919  fourierdlem73  46921  fourierdlem77  46925  fourierdlem83  46931  fourierdlem87  46935  fourierdlem94  46942  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem113  46961  salexct  47076  subsaliuncl  47100  sge0lefi  47140  sge0isum  47169  sge0reuzb  47190  iundjiun  47202  voliunsge0lem  47214  meaiuninc3v  47226  ovnsubaddlem2  47313  hoiqssbllem3  47366  vonioo  47424  vonicc  47427  preimageiingt  47462  preimaleiinlt  47463  issmfle  47487  issmfgt  47498  issmfge  47512  smflimlem2  47514  smfsupmpt  47557  smfinflem  47559  smfinfmpt  47561  smfliminflem  47572  fsupdm  47584  finfdm  47588  ffnafv  47936  iccelpart  48210  sprsymrelfo  48274  mogoldbb  48578  sbgoldbo  48580  iunord  50482  setrec1lem2  50494  pgind  50523  aacllem  50649