Theorem nfra1 3290

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815   ∈ wcel 2146  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2179

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1812  df-nf 1816  df-ral 3081

This theorem is used by:  hbra1  3303  r19.12  3315  nfra2  3365  ralcom2  3366  2reu1  3849  nfss  3906  2reu4lem  4482  iuneqconst  4966  nfii1  4990  mpteq12f  5193  reusv1  5363  reusv2lem1  5364  reusv2lem2  5365  reusv2lem3  5366  ralxfrALT  5381  fvmptss  7017  fompt  7129  ffnfv  7130  riota5f  7415  mpoeq123  7502  tfinds  7881  zfrep6OLD  7977  frrlem4  8321  tfr3  8421  tz7.48-1  8467  tz7.49  8469  naddsuc2  8725  nfixp1  8960  nneneq  9235  scottexOLD  9947  setrec1lem2  9980  dfac2b  10222  infpssrlem4  10397  hsmexlem2  10518  hsmexlem4  10520  domtriomlem  10533  axdc3lem2  10542  axdc3lem4  10544  axdc4lem  10546  zorn2lem5  10591  konigthlem  10666  eltsk2g  10849  dedekind  11486  dedekindle  11487  lble  12282  fsuppmapnn0fiublem  14146  fsuppmapnn0fiub  14147  fsuppmapnn0fiubex  14148  prodeq2ii  16095  fprodle  16178  lcmfunsnlem1  16827  lcmfunsnlem2lem1  16828  lcmfunsnlem2  16830  mreiincl  17781  mreexexd  17837  catpropd  17898  acsmapd  18743  gsummatr01lem4  22988  cpmatmcllem  23051  alexsubALTlem3  24383  isucn2  24612  nosupbnd1  28086  noinfbnd1  28101  bdaypw2n0bndlem  28864  mpteleeOLD  29488  chirred  33012  opreu2reuALT  33130  foresf1o  33157  abrexss  33165  iinabrex  33220  aciunf1lem  33313  nn0min  33468  fprodex01  33472  isarchiofld  33816  elrspunidl  34034  vieta  34268  reff  34527  locfinreflem  34528  cmpcref  34538  zarcmplem  34569  esumcl  34718  measvunilem  34901  measvunilem0  34902  measvuni  34903  voliune  34918  volfiniune  34919  omssubadd  34988  bnj1366  35515  bnj1379  35516  bnj571  35592  bnj1039  35657  bnj1128  35676  bnj1204  35698  bnj1279  35704  bnj1307  35709  bnj1388  35719  bnj1398  35720  bnj1444  35729  bnj1489  35742  bnj1525  35755  srepdf  36044  dfon2lem3  36677  mh-inf3f1  37459  domalom  38470  ralssiun  38473  fvineqsneu  38477  fvineqsneq  38478  heicant  38716  cover2  38792  upixp  38806  indexdom  38811  filbcmb  38817  riotasvd  40156  riotasv2d  40157  riotasv2s  40158  glbconxN  40578  pmapglbx  40969  pmapglb2xN  40972  cdleme26ee  41560  cdlemefr29exN  41602  cdlemefs32sn1aw  41614  cdleme43fsv1snlem  41620  cdleme41sn3a  41633  cdleme32d  41644  cdleme32f  41646  cdleme40m  41667  cdleme40n  41668  cdlemk36  42113  cdlemk38  42115  cdlemkid  42136  cdlemk19x  42143  cdlemk11t  42146  mzpexpmpt  43899  nadd1suc  44537  gneispace  45277  mnuprdlem4  45402  ssralv2  45656  tratrb  45661  modelaxrep  46113  fnchoice  46188  rfcnnnub  46195  uzwo4  46212  ralimralim  46240  suprnmpt  46331  choicefi  46356  axccdom  46377  axccd  46383  rnmptlb  46397  rnmptbddlem  46398  rnmptbd2lem  46402  rnmptbdlem  46409  upbdrech  46463  ssfiunibd  46467  iuneqfzuzlem  46488  infxrunb2  46521  xrralrecnnle  46536  supxrunb3  46552  supxrleubrnmpt  46558  unb2ltle  46567  rexabslelem  46570  allbutfiinf  46572  suprleubrnmpt  46574  uzub  46583  infxrgelbrnmpt  46606  cvgcaule  46643  mccl  46752  climsuse  46762  mullimc  46770  islptre  46773  mullimcf  46777  limcrecl  46783  islpcn  46791  limsupre  46793  limcleqr  46796  addlimc  46800  0ellimcdiv  46801  limclner  46803  climinf2lem  46858  limsupubuz  46865  climinf3  46868  limsupmnflem  46872  limsupmnfuzlem  46878  limsupre3uzlem  46887  climisp  46898  climrescn  46900  climxrrelem  46901  climxrre  46902  xlimmnfv  46986  xlimpnfv  46990  climxlim2lem  46997  cncfioobd  47049  stoweidlem16  47168  stoweidlem28  47180  stoweidlem29  47181  stoweidlem31  47183  stoweidlem35  47187  stoweidlem48  47200  stoweidlem51  47203  stoweidlem52  47204  stoweidlem53  47205  stoweidlem54  47206  stoweidlem56  47208  stoweidlem57  47209  stoweidlem59  47211  stoweidlem60  47212  stoweidlem62  47214  wallispilem3  47219  stirlinglem13  47238  fourierdlem31  47290  fourierdlem39  47298  fourierdlem68  47326  fourierdlem71  47329  fourierdlem73  47331  fourierdlem77  47335  fourierdlem83  47341  fourierdlem87  47345  fourierdlem94  47352  fourierdlem103  47361  fourierdlem104  47362  fourierdlem112  47370  fourierdlem113  47371  salexct  47486  subsaliuncl  47510  sge0lefi  47550  sge0isum  47579  sge0reuzb  47600  iundjiun  47612  voliunsge0lem  47624  meaiuninc3v  47636  ovnsubaddlem2  47723  hoiqssbllem3  47776  vonioo  47834  vonicc  47837  preimageiingt  47872  preimaleiinlt  47873  issmfle  47897  issmfgt  47908  issmfge  47922  smflimlem2  47924  smfsupmpt  47967  smfinflem  47969  smfinfmpt  47971  smfliminflem  47982  fsupdm  47994  finfdm  47998  ffnafv  48383  iccelpart  48657  sprsymrelfo  48721  mogoldbb  49025  sbgoldbo  49027  iunord  51001  pgind  51027  aacllem  51156