Theorem nfra1 3286

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 3077	. 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 3076

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 3077

This theorem is used by:  hbra1  3299  r19.12  3311  nfra2  3361  ralcom2  3362  2reu1  3845  nfss  3924  2reu4lem  4479  iuneqconst  4963  nfii1  4987  mpteq12f  5190  reusv1  5362  reusv2lem1  5363  reusv2lem2  5364  reusv2lem3  5365  ralxfrALT  5380  fvmptss  7000  fompt  7112  ffnfv  7113  riota5f  7399  mpoeq123  7486  tfinds  7857  zfrep6OLD  7953  frrlem4  8289  tfr3  8389  tz7.48-1  8435  tz7.49  8437  naddsuc2  8693  nfixp1  8928  nneneq  9203  scottexOLD  9876  dfac2b  10136  infpssrlem4  10311  hsmexlem2  10432  hsmexlem4  10434  domtriomlem  10447  axdc3lem2  10456  axdc3lem4  10458  axdc4lem  10460  zorn2lem5  10505  konigthlem  10580  eltsk2g  10763  dedekind  11400  dedekindle  11401  lble  12194  fsuppmapnn0fiublem  14057  fsuppmapnn0fiub  14058  fsuppmapnn0fiubex  14059  prodeq2ii  16003  fprodle  16086  lcmfunsnlem1  16730  lcmfunsnlem2lem1  16731  lcmfunsnlem2  16733  mreiincl  17683  mreexexd  17739  catpropd  17800  acsmapd  18645  gsummatr01lem4  22883  cpmatmcllem  22946  alexsubALTlem3  24278  isucn2  24507  nosupbnd1  27953  noinfbnd1  27968  bdaypw2n0bndlem  28731  mpteleeOLD  29355  chirred  32879  opreu2reuALT  32955  foresf1o  32982  abrexss  32990  iinabrex  33045  aciunf1lem  33138  nn0min  33294  fprodex01  33298  isarchiofld  33642  elrspunidl  33859  vieta  34093  reff  34352  locfinreflem  34353  cmpcref  34363  zarcmplem  34394  esumcl  34543  measvunilem  34726  measvunilem0  34727  measvuni  34728  voliune  34743  volfiniune  34744  omssubadd  34814  bnj1366  35341  bnj1379  35342  bnj571  35418  bnj1039  35483  bnj1128  35502  bnj1204  35524  bnj1279  35530  bnj1307  35535  bnj1388  35545  bnj1398  35546  bnj1444  35555  bnj1489  35568  bnj1525  35581  dfon2lem3  36365  mh-inf3f1  37163  domalom  38161  ralssiun  38164  fvineqsneu  38168  fvineqsneq  38169  heicant  38407  cover2  38468  upixp  38482  indexdom  38487  filbcmb  38493  riotasvd  39832  riotasv2d  39833  riotasv2s  39834  glbconxN  40254  pmapglbx  40645  pmapglb2xN  40648  cdleme26ee  41236  cdlemefr29exN  41278  cdlemefs32sn1aw  41290  cdleme43fsv1snlem  41296  cdleme41sn3a  41309  cdleme32d  41320  cdleme32f  41322  cdleme40m  41343  cdleme40n  41344  cdlemk36  41789  cdlemk38  41791  cdlemkid  41812  cdlemk19x  41819  cdlemk11t  41822  mzpexpmpt  43593  nadd1suc  44236  gneispace  44977  mnuprdlem4  45102  ssralv2  45357  tratrb  45362  modelaxrep  45807  fnchoice  45866  rfcnnnub  45873  uzwo4  45890  ralimralim  45918  suprnmpt  46009  choicefi  46034  axccdom  46055  axccd  46061  rnmptlb  46075  rnmptbddlem  46076  rnmptbd2lem  46080  rnmptbdlem  46087  upbdrech  46141  ssfiunibd  46145  iuneqfzuzlem  46167  infxrunb2  46200  xrralrecnnle  46215  supxrunb3  46231  supxrleubrnmpt  46237  unb2ltle  46246  rexabslelem  46249  allbutfiinf  46251  suprleubrnmpt  46253  uzub  46262  infxrgelbrnmpt  46285  cvgcaule  46322  mccl  46431  climsuse  46441  mullimc  46449  islptre  46452  mullimcf  46456  limcrecl  46462  islpcn  46470  limsupre  46472  limcleqr  46475  addlimc  46479  0ellimcdiv  46480  limclner  46482  climinf2lem  46537  limsupubuz  46544  climinf3  46547  limsupmnflem  46551  limsupmnfuzlem  46557  limsupre3uzlem  46566  climisp  46577  climrescn  46579  climxrrelem  46580  climxrre  46581  xlimmnfv  46665  xlimpnfv  46669  climxlim2lem  46676  cncfioobd  46728  stoweidlem16  46847  stoweidlem28  46859  stoweidlem29  46860  stoweidlem31  46862  stoweidlem35  46866  stoweidlem48  46879  stoweidlem51  46882  stoweidlem52  46883  stoweidlem53  46884  stoweidlem54  46885  stoweidlem56  46887  stoweidlem57  46888  stoweidlem59  46890  stoweidlem60  46891  stoweidlem62  46893  wallispilem3  46898  stirlinglem13  46917  fourierdlem31  46969  fourierdlem39  46977  fourierdlem68  47005  fourierdlem71  47008  fourierdlem73  47010  fourierdlem77  47014  fourierdlem83  47020  fourierdlem87  47024  fourierdlem94  47031  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem113  47050  salexct  47165  subsaliuncl  47189  sge0lefi  47229  sge0isum  47258  sge0reuzb  47279  iundjiun  47291  voliunsge0lem  47303  meaiuninc3v  47315  ovnsubaddlem2  47402  hoiqssbllem3  47455  vonioo  47513  vonicc  47516  preimageiingt  47551  preimaleiinlt  47552  issmfle  47576  issmfgt  47587  issmfge  47601  smflimlem2  47603  smfsupmpt  47646  smfinflem  47648  smfinfmpt  47650  smfliminflem  47661  fsupdm  47673  finfdm  47677  ffnafv  48062  iccelpart  48336  sprsymrelfo  48400  mogoldbb  48704  sbgoldbo  48706  iunord  50605  setrec1lem2  50617  pgind  50646  aacllem  50775