Theorem nfra1 3291

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2179

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817  df-ral 3082

This theorem is used by:  hbra1  3304  r19.12  3316  nfra2  3367  ralcom2  3368  2reu1  3852  nfss  3931  2reu4lem  4486  iuneqconst  4970  nfii1  4995  mpteq12f  5198  reusv1  5370  reusv2lem1  5371  reusv2lem2  5372  reusv2lem3  5373  ralxfrALT  5388  fvmptss  7006  fompt  7117  ffnfv  7118  riota5f  7404  mpoeq123  7491  tfinds  7862  zfrep6OLD  7958  frrlem4  8292  tfr3  8392  tz7.48-1  8436  tz7.49  8438  naddsuc2  8694  nfixp1  8922  nneneq  9197  scottexOLD  9870  dfac2b  10130  infpssrlem4  10305  hsmexlem2  10426  hsmexlem4  10428  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  zorn2lem5  10499  konigthlem  10572  eltsk2g  10755  dedekind  11392  dedekindle  11393  lble  12186  fsuppmapnn0fiublem  14048  fsuppmapnn0fiub  14049  fsuppmapnn0fiubex  14050  prodeq2ii  15992  fprodle  16077  lcmfunsnlem1  16721  lcmfunsnlem2lem1  16722  lcmfunsnlem2  16724  mreiincl  17674  mreexexd  17730  catpropd  17791  acsmapd  18636  gsummatr01lem4  22869  cpmatmcllem  22929  alexsubALTlem3  24261  isucn2  24490  nosupbnd1  27933  noinfbnd1  27948  bdaypw2n0bndlem  28711  mpteleeOLD  29304  chirred  32822  opreu2reuALT  32898  foresf1o  32925  abrexss  32933  iinabrex  32989  aciunf1lem  33082  nn0min  33239  fprodex01  33243  isarchiofld  33587  elrspunidl  33804  vieta  34038  reff  34297  locfinreflem  34298  cmpcref  34308  zarcmplem  34339  esumcl  34488  measvunilem  34671  measvunilem0  34672  measvuni  34673  voliune  34688  volfiniune  34689  omssubadd  34759  bnj1366  35286  bnj1379  35287  bnj571  35363  bnj1039  35428  bnj1128  35447  bnj1204  35469  bnj1279  35475  bnj1307  35480  bnj1388  35490  bnj1398  35491  bnj1444  35500  bnj1489  35513  bnj1525  35526  dfon2lem3  36316  domalom  38111  ralssiun  38114  fvineqsneu  38118  fvineqsneq  38119  heicant  38367  cover2  38428  upixp  38442  indexdom  38447  filbcmb  38453  riotasvd  39792  riotasv2d  39793  riotasv2s  39794  glbconxN  40214  pmapglbx  40605  pmapglb2xN  40608  cdleme26ee  41196  cdlemefr29exN  41238  cdlemefs32sn1aw  41250  cdleme43fsv1snlem  41256  cdleme41sn3a  41269  cdleme32d  41280  cdleme32f  41282  cdleme40m  41303  cdleme40n  41304  cdlemk36  41749  cdlemk38  41751  cdlemkid  41772  cdlemk19x  41779  cdlemk11t  41782  mzpexpmpt  43553  nadd1suc  44196  gneispace  44937  mnuprdlem4  45062  ssralv2  45317  tratrb  45322  modelaxrep  45767  fnchoice  45826  rfcnnnub  45833  uzwo4  45850  ralimralim  45878  suprnmpt  45969  choicefi  45994  axccdom  46015  axccd  46021  rnmptlb  46035  rnmptbddlem  46036  rnmptbd2lem  46040  rnmptbdlem  46047  upbdrech  46101  ssfiunibd  46105  iuneqfzuzlem  46127  infxrunb2  46160  xrralrecnnle  46175  supxrunb3  46191  supxrleubrnmpt  46197  unb2ltle  46206  rexabslelem  46209  allbutfiinf  46211  suprleubrnmpt  46213  uzub  46222  infxrgelbrnmpt  46245  cvgcaule  46282  mccl  46391  climsuse  46401  mullimc  46409  islptre  46412  mullimcf  46416  limcrecl  46422  islpcn  46430  limsupre  46432  limcleqr  46435  addlimc  46439  0ellimcdiv  46440  limclner  46442  climinf2lem  46497  limsupubuz  46504  climinf3  46507  limsupmnflem  46511  limsupmnfuzlem  46517  limsupre3uzlem  46526  climisp  46537  climrescn  46539  climxrrelem  46540  climxrre  46541  xlimmnfv  46625  xlimpnfv  46629  climxlim2lem  46636  cncfioobd  46688  stoweidlem16  46807  stoweidlem28  46819  stoweidlem29  46820  stoweidlem31  46822  stoweidlem35  46826  stoweidlem48  46839  stoweidlem51  46842  stoweidlem52  46843  stoweidlem53  46844  stoweidlem54  46845  stoweidlem56  46847  stoweidlem57  46848  stoweidlem59  46850  stoweidlem60  46851  stoweidlem62  46853  wallispilem3  46858  stirlinglem13  46877  fourierdlem31  46929  fourierdlem39  46937  fourierdlem68  46965  fourierdlem71  46968  fourierdlem73  46970  fourierdlem77  46974  fourierdlem83  46980  fourierdlem87  46984  fourierdlem94  46991  fourierdlem103  47000  fourierdlem104  47001  fourierdlem112  47009  fourierdlem113  47010  salexct  47125  subsaliuncl  47149  sge0lefi  47189  sge0isum  47218  sge0reuzb  47239  iundjiun  47251  voliunsge0lem  47263  meaiuninc3v  47275  ovnsubaddlem2  47362  hoiqssbllem3  47415  vonioo  47473  vonicc  47476  preimageiingt  47511  preimaleiinlt  47512  issmfle  47536  issmfgt  47547  issmfge  47561  smflimlem2  47563  smfsupmpt  47606  smfinflem  47608  smfinfmpt  47610  smfliminflem  47621  fsupdm  47633  finfdm  47637  ffnafv  47985  iccelpart  48259  sprsymrelfo  48323  mogoldbb  48627  sbgoldbo  48629  iunord  50530  setrec1lem2  50542  pgind  50571  aacllem  50697