Theorem nfra1 3261

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  3274  r19.12  3286  nfra2  3347  ralcom2  3348  2reu1  3848  nfss  3927  2reu4lem  4477  iuneqconst  4959  nfii1  4985  mpteq12f  5184  reusv1  5343  reusv2lem1  5344  reusv2lem2  5345  reusv2lem3  5346  ralxfrALT  5361  fvmptss  6955  fompt  7065  ffnfv  7066  riota5f  7345  mpoeq123  7432  tfinds  7804  zfrep6  7901  frrlem4  8233  tfr3  8332  tz7.48-1  8376  tz7.49  8378  naddsuc2  8631  nfixp1  8860  nneneq  9134  scottex  9801  dfac2b  10045  infpssrlem4  10220  hsmexlem2  10341  hsmexlem4  10343  domtriomlem  10356  axdc3lem2  10365  axdc3lem4  10367  axdc4lem  10369  zorn2lem5  10414  konigthlem  10483  eltsk2g  10666  dedekind  11300  dedekindle  11301  lble  12098  fsuppmapnn0fiublem  13917  fsuppmapnn0fiub  13918  fsuppmapnn0fiubex  13919  prodeq2ii  15838  fprodle  15923  lcmfunsnlem1  16568  lcmfunsnlem2lem1  16569  lcmfunsnlem2  16571  mreiincl  17519  mreexexd  17575  catpropd  17636  acsmapd  18481  gsummatr01lem4  22606  cpmatmcllem  22666  alexsubALTlem3  23997  isucn2  24226  nosupbnd1  27686  noinfbnd1  27701  bdaypw2n0bndlem  28463  mpteleeOLD  28972  chirred  32474  opreu2reuALT  32554  foresf1o  32582  abrexss  32590  iinabrex  32647  aciunf1lem  32743  nn0min  32903  fprodex01  32908  isarchiofld  33283  elrspunidl  33511  vieta  33738  reff  33998  locfinreflem  33999  cmpcref  34009  zarcmplem  34040  esumcl  34189  measvunilem  34371  measvunilem0  34372  measvuni  34373  voliune  34388  volfiniune  34389  omssubadd  34459  bnj1366  34987  bnj1379  34988  bnj571  35064  bnj1039  35129  bnj1128  35148  bnj1204  35170  bnj1279  35176  bnj1307  35181  bnj1388  35191  bnj1398  35192  bnj1444  35201  bnj1489  35214  bnj1525  35227  dfon2lem3  35979  domalom  37611  ralssiun  37614  fvineqsneu  37618  fvineqsneq  37619  heicant  37858  cover2  37918  upixp  37932  indexdom  37937  filbcmb  37943  riotasvd  39284  riotasv2d  39285  riotasv2s  39286  glbconxN  39706  pmapglbx  40097  pmapglb2xN  40100  cdleme26ee  40688  cdlemefr29exN  40730  cdlemefs32sn1aw  40742  cdleme43fsv1snlem  40748  cdleme41sn3a  40761  cdleme32d  40772  cdleme32f  40774  cdleme40m  40795  cdleme40n  40796  cdlemk36  41241  cdlemk38  41243  cdlemkid  41264  cdlemk19x  41271  cdlemk11t  41274  mzpexpmpt  43054  nadd1suc  43701  gneispace  44442  mnuprdlem4  44583  ssralv2  44839  tratrb  44844  modelaxrep  45289  fnchoice  45341  rfcnnnub  45348  uzwo4  45365  ralimralim  45393  suprnmpt  45485  choicefi  45511  axccdom  45533  axccd  45540  rnmptlb  45554  rnmptbddlem  45555  rnmptbd2lem  45559  rnmptbdlem  45566  upbdrech  45620  ssfiunibd  45624  iuneqfzuzlem  45646  infxrunb2  45679  xrralrecnnle  45694  supxrunb3  45710  supxrleubrnmpt  45717  unb2ltle  45726  rexabslelem  45729  allbutfiinf  45731  suprleubrnmpt  45733  uzub  45742  infxrgelbrnmpt  45765  cvgcaule  45802  mccl  45911  climsuse  45921  mullimc  45929  islptre  45932  mullimcf  45936  limcrecl  45942  islpcn  45950  limsupre  45952  limcleqr  45955  addlimc  45959  0ellimcdiv  45960  limclner  45962  climinf2lem  46017  limsupubuz  46024  climinf3  46027  limsupmnflem  46031  limsupmnfuzlem  46037  limsupre3uzlem  46046  climisp  46057  climrescn  46059  climxrrelem  46060  climxrre  46061  xlimmnfv  46145  xlimpnfv  46149  climxlim2lem  46156  cncfioobd  46208  stoweidlem16  46327  stoweidlem28  46339  stoweidlem29  46340  stoweidlem31  46342  stoweidlem35  46346  stoweidlem48  46359  stoweidlem51  46362  stoweidlem52  46363  stoweidlem53  46364  stoweidlem54  46365  stoweidlem56  46367  stoweidlem57  46368  stoweidlem59  46370  stoweidlem60  46371  stoweidlem62  46373  wallispilem3  46378  stirlinglem13  46397  fourierdlem31  46449  fourierdlem39  46457  fourierdlem68  46485  fourierdlem71  46488  fourierdlem73  46490  fourierdlem77  46494  fourierdlem83  46500  fourierdlem87  46504  fourierdlem94  46511  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  fourierdlem113  46530  salexct  46645  subsaliuncl  46669  sge0lefi  46709  sge0isum  46738  sge0reuzb  46759  iundjiun  46771  voliunsge0lem  46783  meaiuninc3v  46795  ovnsubaddlem2  46882  hoiqssbllem3  46935  vonioo  46993  vonicc  46996  preimageiingt  47031  preimaleiinlt  47032  issmfle  47056  issmfgt  47067  issmfge  47081  smflimlem2  47083  smfsupmpt  47126  smfinflem  47128  smfinfmpt  47130  smfliminflem  47141  fsupdm  47153  finfdm  47157  ffnafv  47484  iccelpart  47746  sprsymrelfo  47810  mogoldbb  48098  sbgoldbo  48100  iunord  49988  setrec1lem2  50000  pgind  50029  aacllem  50113