Theorem nfra1 3295

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

Syntax hints:   → wi 4  ∀wal 1565  Ⅎwnf 1810   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1807  df-nf 1811  df-ral 3086

This theorem is referenced by:  hbra1  3308  r19.12  3320  nfra2  3372  ralcom2  3373  2reu1  3859  nfss  3938  2reu4lem  4489  iuneqconst  4972  nfii1  4997  mpteq12f  5200  reusv1  5369  reusv2lem1  5370  reusv2lem2  5371  reusv2lem3  5372  ralxfrALT  5387  fvmptss  7003  fompt  7114  ffnfv  7115  riota5f  7396  mpoeq123  7483  tfinds  7856  zfrep6OLD  7952  frrlem4  8286  tfr3  8386  tz7.48-1  8430  tz7.49  8432  naddsuc2  8688  nfixp1  8916  nneneq  9190  scottex  9859  dfac2b  10114  infpssrlem4  10290  hsmexlem2  10411  hsmexlem4  10413  domtriomlem  10426  axdc3lem2  10435  axdc3lem4  10437  axdc4lem  10439  zorn2lem5  10484  konigthlem  10553  eltsk2g  10736  dedekind  11373  dedekindle  11374  lble  12167  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  fsuppmapnn0fiubex  14028  prodeq2ii  15965  fprodle  16050  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  lcmfunsnlem2  16698  mreiincl  17648  mreexexd  17704  catpropd  17765  acsmapd  18610  gsummatr01lem4  22784  cpmatmcllem  22844  alexsubALTlem3  24175  isucn2  24404  nosupbnd1  27844  noinfbnd1  27859  bdaypw2n0bndlem  28622  mpteleeOLD  29186  chirred  32688  opreu2reuALT  32764  foresf1o  32791  abrexss  32799  iinabrex  32855  aciunf1lem  32948  nn0min  33106  fprodex01  33110  isarchiofld  33460  elrspunidl  33680  vieta  33915  reff  34174  locfinreflem  34175  cmpcref  34185  zarcmplem  34216  esumcl  34365  measvunilem  34547  measvunilem0  34548  measvuni  34549  voliune  34564  volfiniune  34565  omssubadd  34635  bnj1366  35162  bnj1379  35163  bnj571  35239  bnj1039  35304  bnj1128  35323  bnj1204  35345  bnj1279  35351  bnj1307  35356  bnj1388  35366  bnj1398  35367  bnj1444  35376  bnj1489  35389  bnj1525  35402  dfon2lem3  36208  domalom  37972  ralssiun  37975  fvineqsneu  37979  fvineqsneq  37980  heicant  38228  cover2  38288  upixp  38302  indexdom  38307  filbcmb  38313  riotasvd  39654  riotasv2d  39655  riotasv2s  39656  glbconxN  40076  pmapglbx  40467  pmapglb2xN  40470  cdleme26ee  41058  cdlemefr29exN  41100  cdlemefs32sn1aw  41112  cdleme43fsv1snlem  41118  cdleme41sn3a  41131  cdleme32d  41142  cdleme32f  41144  cdleme40m  41165  cdleme40n  41166  cdlemk36  41611  cdlemk38  41613  cdlemkid  41634  cdlemk19x  41641  cdlemk11t  41644  mzpexpmpt  43402  nadd1suc  44045  gneispace  44786  mnuprdlem4  44911  ssralv2  45166  tratrb  45171  modelaxrep  45616  fnchoice  45675  rfcnnnub  45682  uzwo4  45699  ralimralim  45727  suprnmpt  45818  choicefi  45843  axccdom  45864  axccd  45870  rnmptlb  45884  rnmptbddlem  45885  rnmptbd2lem  45889  rnmptbdlem  45896  upbdrech  45950  ssfiunibd  45954  iuneqfzuzlem  45976  infxrunb2  46009  xrralrecnnle  46024  supxrunb3  46040  supxrleubrnmpt  46046  unb2ltle  46055  rexabslelem  46058  allbutfiinf  46060  suprleubrnmpt  46062  uzub  46071  infxrgelbrnmpt  46094  cvgcaule  46131  mccl  46240  climsuse  46250  mullimc  46258  islptre  46261  mullimcf  46265  limcrecl  46271  islpcn  46279  limsupre  46281  limcleqr  46284  addlimc  46288  0ellimcdiv  46289  limclner  46291  climinf2lem  46346  limsupubuz  46353  climinf3  46356  limsupmnflem  46360  limsupmnfuzlem  46366  limsupre3uzlem  46375  climisp  46386  climrescn  46388  climxrrelem  46389  climxrre  46390  xlimmnfv  46474  xlimpnfv  46478  climxlim2lem  46485  cncfioobd  46537  stoweidlem16  46656  stoweidlem28  46668  stoweidlem29  46669  stoweidlem31  46671  stoweidlem35  46675  stoweidlem48  46688  stoweidlem51  46691  stoweidlem52  46692  stoweidlem53  46693  stoweidlem54  46694  stoweidlem56  46696  stoweidlem57  46697  stoweidlem59  46699  stoweidlem60  46700  stoweidlem62  46702  wallispilem3  46707  stirlinglem13  46726  fourierdlem31  46778  fourierdlem39  46786  fourierdlem68  46814  fourierdlem71  46817  fourierdlem73  46819  fourierdlem77  46823  fourierdlem83  46829  fourierdlem87  46833  fourierdlem94  46840  fourierdlem103  46849  fourierdlem104  46850  fourierdlem112  46858  fourierdlem113  46859  salexct  46974  subsaliuncl  46998  sge0lefi  47038  sge0isum  47067  sge0reuzb  47088  iundjiun  47100  voliunsge0lem  47112  meaiuninc3v  47124  ovnsubaddlem2  47211  hoiqssbllem3  47264  vonioo  47322  vonicc  47325  preimageiingt  47360  preimaleiinlt  47361  issmfle  47385  issmfgt  47396  issmfge  47410  smflimlem2  47412  smfsupmpt  47455  smfinflem  47457  smfinfmpt  47459  smfliminflem  47470  fsupdm  47482  finfdm  47486  ffnafv  47831  iccelpart  48105  sprsymrelfo  48169  mogoldbb  48473  sbgoldbo  48475  iunord  50373  setrec1lem2  50385  pgind  50414  aacllem  50509