Theorem nfra1 3282

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787  df-ral 3063

This theorem is referenced by:  hbra1  3299  r19.12  3312  r19.12OLD  3313  nfra2wOLDOLD  3320  nfra2  3373  ralcom2  3374  2reu1  3891  nfss  3974  rspn0OLD  4353  ralidmOLD  4515  2reu4lem  4525  iuneqconst  5008  nfii1  5032  dfiun2gOLD  5034  mpteq12f  5236  reusv1  5395  reusv2lem1  5396  reusv2lem2  5397  reusv2lem3  5398  ralxfrALT  5413  fvmptss  7008  ffnfv  7115  riota5f  7391  mpoeq123  7478  tfinds  7846  peano5OLD  7882  zfrep6  7938  frrlem4  8271  wfrlem4OLD  8309  tfr3  8396  tz7.48-1  8440  tz7.49  8442  nfixp1  8909  nneneq  9206  nneneqOLD  9218  scottex  9877  dfac2b  10122  infpssrlem4  10298  hsmexlem2  10419  hsmexlem4  10421  domtriomlem  10434  axdc3lem2  10443  axdc3lem4  10445  axdc4lem  10447  zorn2lem5  10492  konigthlem  10560  eltsk2g  10743  dedekind  11374  dedekindle  11375  lble  12163  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  fsuppmapnn0fiubex  13954  prodeq2ii  15854  fprodle  15937  lcmfunsnlem1  16571  lcmfunsnlem2lem1  16572  lcmfunsnlem2  16574  mreiincl  17537  mreexexd  17589  catpropd  17650  acsmapd  18504  gsummatr01lem4  22152  cpmatmcllem  22212  alexsubALTlem3  23545  isucn2  23776  nosupbnd1  27207  noinfbnd1  27222  mptelee  28143  chirred  31636  opreu2reuALT  31705  foresf1o  31730  abrexss  31737  iinabrex  31788  aciunf1lem  31875  nn0min  32014  fprodex01  32019  isarchiofld  32424  elrspunidl  32535  reff  32808  locfinreflem  32809  cmpcref  32819  zarcmplem  32850  esumcl  33017  measvunilem  33199  measvunilem0  33200  measvuni  33201  voliune  33216  volfiniune  33217  omssubadd  33288  bnj1366  33829  bnj1379  33830  bnj571  33906  bnj1039  33971  bnj1128  33990  bnj1204  34012  bnj1279  34018  bnj1307  34023  bnj1388  34033  bnj1398  34034  bnj1444  34043  bnj1489  34056  bnj1525  34069  dfon2lem3  34746  domalom  36274  ralssiun  36277  fvineqsneu  36281  fvineqsneq  36282  heicant  36512  cover2  36572  upixp  36586  indexdom  36591  filbcmb  36597  riotasvd  37815  riotasv2d  37816  riotasv2s  37817  glbconxN  38238  pmapglbx  38629  pmapglb2xN  38632  cdleme26ee  39220  cdlemefr29exN  39262  cdlemefs32sn1aw  39274  cdleme43fsv1snlem  39280  cdleme41sn3a  39293  cdleme32d  39304  cdleme32f  39306  cdleme40m  39327  cdleme40n  39328  cdlemk36  39773  cdlemk38  39775  cdlemkid  39796  cdlemk19x  39803  cdlemk11t  39806  mzpexpmpt  41469  nadd1suc  42128  naddsuc2  42129  gneispace  42871  mnuprdlem4  43020  ssralv2  43278  tratrb  43283  fnchoice  43699  rfcnnnub  43706  uzwo4  43726  ralimralim  43756  suprnmpt  43856  fompt  43876  choicefi  43885  axccdom  43907  axccd  43914  rnmptlb  43933  rnmptbddlem  43934  rnmptbd2lem  43939  rnmptbdlem  43946  upbdrech  44002  ssfiunibd  44006  iuneqfzuzlem  44031  infxrunb2  44065  xrralrecnnle  44080  supxrunb3  44096  supxrleubrnmpt  44103  unb2ltle  44112  rexabslelem  44115  allbutfiinf  44117  suprleubrnmpt  44119  uzub  44128  infxrgelbrnmpt  44151  cvgcaule  44189  mccl  44301  climsuse  44311  mullimc  44319  islptre  44322  mullimcf  44326  limcrecl  44332  islpcn  44342  limsupre  44344  limcleqr  44347  addlimc  44351  0ellimcdiv  44352  limclner  44354  climinf2lem  44409  limsupubuz  44416  climinf3  44419  limsupmnflem  44423  limsupmnfuzlem  44429  limsupre3uzlem  44438  climisp  44449  climrescn  44451  climxrrelem  44452  climxrre  44453  xlimmnfv  44537  xlimpnfv  44541  climxlim2lem  44548  cncfioobd  44600  stoweidlem16  44719  stoweidlem28  44731  stoweidlem29  44732  stoweidlem31  44734  stoweidlem35  44738  stoweidlem48  44751  stoweidlem51  44754  stoweidlem52  44755  stoweidlem53  44756  stoweidlem54  44757  stoweidlem56  44759  stoweidlem57  44760  stoweidlem59  44762  stoweidlem60  44763  stoweidlem62  44765  wallispilem3  44770  stirlinglem13  44789  fourierdlem31  44841  fourierdlem39  44849  fourierdlem68  44877  fourierdlem71  44880  fourierdlem73  44882  fourierdlem77  44886  fourierdlem83  44892  fourierdlem87  44896  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  fourierdlem112  44921  fourierdlem113  44922  salexct  45037  subsaliuncl  45061  sge0lefi  45101  sge0isum  45130  sge0reuzb  45151  iundjiun  45163  voliunsge0lem  45175  meaiuninc3v  45187  ovnsubaddlem2  45274  hoiqssbllem3  45327  vonioo  45385  vonicc  45388  preimageiingt  45423  preimaleiinlt  45424  issmfle  45448  issmfgt  45459  issmfge  45473  smflimlem2  45475  smfsupmpt  45518  smfinflem  45520  smfinfmpt  45522  smfliminflem  45533  fsupdm  45545  finfdm  45549  ffnafv  45866  iccelpart  46088  sprsymrelfo  46152  mogoldbb  46440  sbgoldbo  46442  iunord  47675  setrec1lem2  47687  pgind  47716  aacllem  47802