Theorem nfra1 3266

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784  df-ral 3052

This theorem is referenced by:  hbra1  3281  r19.12  3294  nfra2  3355  ralcom2  3356  2reu1  3872  nfss  3951  2reu4lem  4497  iuneqconst  4979  nfii1  5005  dfiun2gOLD  5007  mpteq12f  5205  reusv1  5367  reusv2lem1  5368  reusv2lem2  5369  reusv2lem3  5370  ralxfrALT  5385  fvmptss  6997  fompt  7107  ffnfv  7108  riota5f  7388  mpoeq123  7477  tfinds  7853  zfrep6  7951  frrlem4  8286  wfrlem4OLD  8324  tfr3  8411  tz7.48-1  8455  tz7.49  8457  naddsuc2  8711  nfixp1  8930  nneneq  9218  scottex  9897  dfac2b  10143  infpssrlem4  10318  hsmexlem2  10439  hsmexlem4  10441  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  zorn2lem5  10512  konigthlem  10580  eltsk2g  10763  dedekind  11396  dedekindle  11397  lble  12192  fsuppmapnn0fiublem  14006  fsuppmapnn0fiub  14007  fsuppmapnn0fiubex  14008  prodeq2ii  15925  fprodle  16010  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  mreiincl  17606  mreexexd  17658  catpropd  17719  acsmapd  18562  gsummatr01lem4  22594  cpmatmcllem  22654  alexsubALTlem3  23985  isucn2  24215  nosupbnd1  27676  noinfbnd1  27691  mptelee  28820  chirred  32322  opreu2reuALT  32404  foresf1o  32431  abrexss  32439  iinabrex  32496  aciunf1lem  32586  nn0min  32745  fprodex01  32750  isarchiofld  33285  elrspunidl  33389  reff  33816  locfinreflem  33817  cmpcref  33827  zarcmplem  33858  esumcl  34007  measvunilem  34189  measvunilem0  34190  measvuni  34191  voliune  34206  volfiniune  34207  omssubadd  34278  bnj1366  34806  bnj1379  34807  bnj571  34883  bnj1039  34948  bnj1128  34967  bnj1204  34989  bnj1279  34995  bnj1307  35000  bnj1388  35010  bnj1398  35011  bnj1444  35020  bnj1489  35033  bnj1525  35046  dfon2lem3  35749  domalom  37368  ralssiun  37371  fvineqsneu  37375  fvineqsneq  37376  heicant  37625  cover2  37685  upixp  37699  indexdom  37704  filbcmb  37710  riotasvd  38920  riotasv2d  38921  riotasv2s  38922  glbconxN  39343  pmapglbx  39734  pmapglb2xN  39737  cdleme26ee  40325  cdlemefr29exN  40367  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32d  40409  cdleme32f  40411  cdleme40m  40432  cdleme40n  40433  cdlemk36  40878  cdlemk38  40880  cdlemkid  40901  cdlemk19x  40908  cdlemk11t  40911  mzpexpmpt  42715  nadd1suc  43363  gneispace  44105  mnuprdlem4  44247  ssralv2  44504  tratrb  44509  modelaxrep  44954  fnchoice  45001  rfcnnnub  45008  uzwo4  45025  ralimralim  45053  suprnmpt  45146  choicefi  45172  axccdom  45194  axccd  45201  rnmptlb  45215  rnmptbddlem  45216  rnmptbd2lem  45220  rnmptbdlem  45227  upbdrech  45282  ssfiunibd  45286  iuneqfzuzlem  45309  infxrunb2  45343  xrralrecnnle  45358  supxrunb3  45374  supxrleubrnmpt  45381  unb2ltle  45390  rexabslelem  45393  allbutfiinf  45395  suprleubrnmpt  45397  uzub  45406  infxrgelbrnmpt  45429  cvgcaule  45466  mccl  45575  climsuse  45585  mullimc  45593  islptre  45596  mullimcf  45600  limcrecl  45606  islpcn  45616  limsupre  45618  limcleqr  45621  addlimc  45625  0ellimcdiv  45626  limclner  45628  climinf2lem  45683  limsupubuz  45690  climinf3  45693  limsupmnflem  45697  limsupmnfuzlem  45703  limsupre3uzlem  45712  climisp  45723  climrescn  45725  climxrrelem  45726  climxrre  45727  xlimmnfv  45811  xlimpnfv  45815  climxlim2lem  45822  cncfioobd  45874  stoweidlem16  45993  stoweidlem28  46005  stoweidlem29  46006  stoweidlem31  46008  stoweidlem35  46012  stoweidlem48  46025  stoweidlem51  46028  stoweidlem52  46029  stoweidlem53  46030  stoweidlem54  46031  stoweidlem56  46033  stoweidlem57  46034  stoweidlem59  46036  stoweidlem60  46037  stoweidlem62  46039  wallispilem3  46044  stirlinglem13  46063  fourierdlem31  46115  fourierdlem39  46123  fourierdlem68  46151  fourierdlem71  46154  fourierdlem73  46156  fourierdlem77  46160  fourierdlem83  46166  fourierdlem87  46170  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem113  46196  salexct  46311  subsaliuncl  46335  sge0lefi  46375  sge0isum  46404  sge0reuzb  46425  iundjiun  46437  voliunsge0lem  46449  meaiuninc3v  46461  ovnsubaddlem2  46548  hoiqssbllem3  46601  vonioo  46659  vonicc  46662  preimageiingt  46697  preimaleiinlt  46698  issmfle  46722  issmfgt  46733  issmfge  46747  smflimlem2  46749  smfsupmpt  46792  smfinflem  46794  smfinfmpt  46796  smfliminflem  46807  fsupdm  46819  finfdm  46823  ffnafv  47148  iccelpart  47395  sprsymrelfo  47459  mogoldbb  47747  sbgoldbo  47749  iunord  49488  setrec1lem2  49500  pgind  49529  aacllem  49613