Theorem nfra1 3287

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2178

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817  df-ral 3078

This theorem is used by:  hbra1  3300  r19.12  3312  nfra2  3362  ralcom2  3363  2reu1  3845  nfss  3924  2reu4lem  4479  iuneqconst  4963  nfii1  4987  mpteq12f  5190  reusv1  5359  reusv2lem1  5360  reusv2lem2  5361  reusv2lem3  5362  ralxfrALT  5377  fvmptss  7006  fompt  7118  ffnfv  7119  riota5f  7405  mpoeq123  7492  tfinds  7871  zfrep6OLD  7967  frrlem4  8307  tfr3  8407  tz7.48-1  8453  tz7.49  8455  naddsuc2  8711  nfixp1  8946  nneneq  9221  scottexOLD  9934  setrec1lem2  9967  dfac2b  10209  infpssrlem4  10384  hsmexlem2  10505  hsmexlem4  10507  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  zorn2lem5  10578  konigthlem  10653  eltsk2g  10836  dedekind  11473  dedekindle  11474  lble  12269  fsuppmapnn0fiublem  14133  fsuppmapnn0fiub  14134  fsuppmapnn0fiubex  14135  prodeq2ii  16080  fprodle  16163  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2  16815  mreiincl  17766  mreexexd  17822  catpropd  17883  acsmapd  18728  gsummatr01lem4  22973  cpmatmcllem  23036  alexsubALTlem3  24368  isucn2  24597  nosupbnd1  28071  noinfbnd1  28086  bdaypw2n0bndlem  28849  mpteleeOLD  29473  chirred  32997  opreu2reuALT  33073  foresf1o  33100  abrexss  33108  iinabrex  33163  aciunf1lem  33256  nn0min  33412  fprodex01  33416  isarchiofld  33760  elrspunidl  33978  vieta  34212  reff  34471  locfinreflem  34472  cmpcref  34482  zarcmplem  34513  esumcl  34662  measvunilem  34845  measvunilem0  34846  measvuni  34847  voliune  34862  volfiniune  34863  omssubadd  34932  bnj1366  35459  bnj1379  35460  bnj571  35536  bnj1039  35601  bnj1128  35620  bnj1204  35642  bnj1279  35648  bnj1307  35653  bnj1388  35663  bnj1398  35664  bnj1444  35673  bnj1489  35686  bnj1525  35699  dfon2lem3  36547  mh-inf3f1  37329  domalom  38327  ralssiun  38330  fvineqsneu  38334  fvineqsneq  38335  heicant  38573  cover2  38649  upixp  38663  indexdom  38668  filbcmb  38674  riotasvd  40013  riotasv2d  40014  riotasv2s  40015  glbconxN  40435  pmapglbx  40826  pmapglb2xN  40829  cdleme26ee  41417  cdlemefr29exN  41459  cdlemefs32sn1aw  41471  cdleme43fsv1snlem  41477  cdleme41sn3a  41490  cdleme32d  41501  cdleme32f  41503  cdleme40m  41524  cdleme40n  41525  cdlemk36  41970  cdlemk38  41972  cdlemkid  41993  cdlemk19x  42000  cdlemk11t  42003  mzpexpmpt  43755  nadd1suc  44393  gneispace  45133  mnuprdlem4  45258  ssralv2  45513  tratrb  45518  modelaxrep  45970  fnchoice  46045  rfcnnnub  46052  uzwo4  46069  ralimralim  46097  suprnmpt  46188  choicefi  46213  axccdom  46234  axccd  46240  rnmptlb  46254  rnmptbddlem  46255  rnmptbd2lem  46259  rnmptbdlem  46266  upbdrech  46320  ssfiunibd  46324  iuneqfzuzlem  46345  infxrunb2  46378  xrralrecnnle  46393  supxrunb3  46409  supxrleubrnmpt  46415  unb2ltle  46424  rexabslelem  46427  allbutfiinf  46429  suprleubrnmpt  46431  uzub  46440  infxrgelbrnmpt  46463  cvgcaule  46500  mccl  46609  climsuse  46619  mullimc  46627  islptre  46630  mullimcf  46634  limcrecl  46640  islpcn  46648  limsupre  46650  limcleqr  46653  addlimc  46657  0ellimcdiv  46658  limclner  46660  climinf2lem  46715  limsupubuz  46722  climinf3  46725  limsupmnflem  46729  limsupmnfuzlem  46735  limsupre3uzlem  46744  climisp  46755  climrescn  46757  climxrrelem  46758  climxrre  46759  xlimmnfv  46843  xlimpnfv  46847  climxlim2lem  46854  cncfioobd  46906  stoweidlem16  47025  stoweidlem28  47037  stoweidlem29  47038  stoweidlem31  47040  stoweidlem35  47044  stoweidlem48  47057  stoweidlem51  47060  stoweidlem52  47061  stoweidlem53  47062  stoweidlem54  47063  stoweidlem56  47065  stoweidlem57  47066  stoweidlem59  47068  stoweidlem60  47069  stoweidlem62  47071  wallispilem3  47076  stirlinglem13  47095  fourierdlem31  47147  fourierdlem39  47155  fourierdlem68  47183  fourierdlem71  47186  fourierdlem73  47188  fourierdlem77  47192  fourierdlem83  47198  fourierdlem87  47202  fourierdlem94  47209  fourierdlem103  47218  fourierdlem104  47219  fourierdlem112  47227  fourierdlem113  47228  salexct  47343  subsaliuncl  47367  sge0lefi  47407  sge0isum  47436  sge0reuzb  47457  iundjiun  47469  voliunsge0lem  47481  meaiuninc3v  47493  ovnsubaddlem2  47580  hoiqssbllem3  47633  vonioo  47691  vonicc  47694  preimageiingt  47729  preimaleiinlt  47730  issmfle  47754  issmfgt  47765  issmfge  47779  smflimlem2  47781  smfsupmpt  47824  smfinflem  47826  smfinfmpt  47828  smfliminflem  47839  fsupdm  47851  finfdm  47855  ffnafv  48240  iccelpart  48514  sprsymrelfo  48578  mogoldbb  48882  sbgoldbo  48884  iunord  50783  pgind  50809  aacllem  50938