Theorem nfra1 3262

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  hbra1  3275  r19.12  3287  nfra2  3339  ralcom2  3340  2reu1  3836  nfss  3915  2reu4lem  4464  iuneqconst  4946  nfii1  4972  mpteq12f  5171  reusv1  5336  reusv2lem1  5337  reusv2lem2  5338  reusv2lem3  5339  ralxfrALT  5354  fvmptss  6956  fompt  7066  ffnfv  7067  riota5f  7347  mpoeq123  7434  tfinds  7806  zfrep6OLD  7903  frrlem4  8234  tfr3  8333  tz7.48-1  8377  tz7.49  8379  naddsuc2  8632  nfixp1  8861  nneneq  9135  scottex  9804  dfac2b  10048  infpssrlem4  10223  hsmexlem2  10344  hsmexlem4  10346  domtriomlem  10359  axdc3lem2  10368  axdc3lem4  10370  axdc4lem  10372  zorn2lem5  10417  konigthlem  10486  eltsk2g  10669  dedekind  11304  dedekindle  11305  lble  12103  fsuppmapnn0fiublem  13947  fsuppmapnn0fiub  13948  fsuppmapnn0fiubex  13949  prodeq2ii  15871  fprodle  15956  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2  16604  mreiincl  17553  mreexexd  17609  catpropd  17670  acsmapd  18515  gsummatr01lem4  22637  cpmatmcllem  22697  alexsubALTlem3  24028  isucn2  24257  nosupbnd1  27696  noinfbnd1  27711  bdaypw2n0bndlem  28473  mpteleeOLD  28982  chirred  32485  opreu2reuALT  32565  foresf1o  32593  abrexss  32601  iinabrex  32658  aciunf1lem  32754  nn0min  32913  fprodex01  32917  isarchiofld  33279  elrspunidl  33507  vieta  33743  reff  34003  locfinreflem  34004  cmpcref  34014  zarcmplem  34045  esumcl  34194  measvunilem  34376  measvunilem0  34377  measvuni  34378  voliune  34393  volfiniune  34394  omssubadd  34464  bnj1366  34991  bnj1379  34992  bnj571  35068  bnj1039  35133  bnj1128  35152  bnj1204  35174  bnj1279  35180  bnj1307  35185  bnj1388  35195  bnj1398  35196  bnj1444  35205  bnj1489  35218  bnj1525  35231  dfon2lem3  35985  domalom  37738  ralssiun  37741  fvineqsneu  37745  fvineqsneq  37746  heicant  37994  cover2  38054  upixp  38068  indexdom  38073  filbcmb  38079  riotasvd  39420  riotasv2d  39421  riotasv2s  39422  glbconxN  39842  pmapglbx  40233  pmapglb2xN  40236  cdleme26ee  40824  cdlemefr29exN  40866  cdlemefs32sn1aw  40878  cdleme43fsv1snlem  40884  cdleme41sn3a  40897  cdleme32d  40908  cdleme32f  40910  cdleme40m  40931  cdleme40n  40932  cdlemk36  41377  cdlemk38  41379  cdlemkid  41400  cdlemk19x  41407  cdlemk11t  41410  mzpexpmpt  43195  nadd1suc  43842  gneispace  44583  mnuprdlem4  44724  ssralv2  44980  tratrb  44985  modelaxrep  45430  fnchoice  45482  rfcnnnub  45489  uzwo4  45506  ralimralim  45534  suprnmpt  45626  choicefi  45651  axccdom  45673  axccd  45680  rnmptlb  45694  rnmptbddlem  45695  rnmptbd2lem  45699  rnmptbdlem  45706  upbdrech  45760  ssfiunibd  45764  iuneqfzuzlem  45786  infxrunb2  45819  xrralrecnnle  45834  supxrunb3  45850  supxrleubrnmpt  45856  unb2ltle  45865  rexabslelem  45868  allbutfiinf  45870  suprleubrnmpt  45872  uzub  45881  infxrgelbrnmpt  45904  cvgcaule  45941  mccl  46050  climsuse  46060  mullimc  46068  islptre  46071  mullimcf  46075  limcrecl  46081  islpcn  46089  limsupre  46091  limcleqr  46094  addlimc  46098  0ellimcdiv  46099  limclner  46101  climinf2lem  46156  limsupubuz  46163  climinf3  46166  limsupmnflem  46170  limsupmnfuzlem  46176  limsupre3uzlem  46185  climisp  46196  climrescn  46198  climxrrelem  46199  climxrre  46200  xlimmnfv  46284  xlimpnfv  46288  climxlim2lem  46295  cncfioobd  46347  stoweidlem16  46466  stoweidlem28  46478  stoweidlem29  46479  stoweidlem31  46481  stoweidlem35  46485  stoweidlem48  46498  stoweidlem51  46501  stoweidlem52  46502  stoweidlem53  46503  stoweidlem54  46504  stoweidlem56  46506  stoweidlem57  46507  stoweidlem59  46509  stoweidlem60  46510  stoweidlem62  46512  wallispilem3  46517  stirlinglem13  46536  fourierdlem31  46588  fourierdlem39  46596  fourierdlem68  46624  fourierdlem71  46627  fourierdlem73  46629  fourierdlem77  46633  fourierdlem83  46639  fourierdlem87  46643  fourierdlem94  46650  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  salexct  46784  subsaliuncl  46808  sge0lefi  46848  sge0isum  46877  sge0reuzb  46898  iundjiun  46910  voliunsge0lem  46922  meaiuninc3v  46934  ovnsubaddlem2  47021  hoiqssbllem3  47074  vonioo  47132  vonicc  47135  preimageiingt  47170  preimaleiinlt  47171  issmfle  47195  issmfgt  47206  issmfge  47220  smflimlem2  47222  smfsupmpt  47265  smfinflem  47267  smfinfmpt  47269  smfliminflem  47280  fsupdm  47292  finfdm  47296  ffnafv  47635  iccelpart  47909  sprsymrelfo  47973  mogoldbb  48277  sbgoldbo  48279  iunord  50167  setrec1lem2  50179  pgind  50208  aacllem  50292