Theorem nfra1 3290

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067

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

This theorem depends on definitions:  df-bi 207  df-or 847  df-ex 1778  df-nf 1782  df-ral 3068

This theorem is referenced by:  hbra1  3307  r19.12  3320  r19.12OLD  3321  nfra2wOLDOLD  3329  nfra2  3384  ralcom2  3385  2reu1  3919  nfss  4001  2reu4lem  4545  iuneqconst  5026  nfii1  5052  dfiun2gOLD  5054  mpteq12f  5254  reusv1  5415  reusv2lem1  5416  reusv2lem2  5417  reusv2lem3  5418  ralxfrALT  5433  fvmptss  7041  fompt  7152  ffnfv  7153  riota5f  7433  mpoeq123  7522  tfinds  7897  peano5OLD  7933  zfrep6  7995  frrlem4  8330  wfrlem4OLD  8368  tfr3  8455  tz7.48-1  8499  tz7.49  8501  naddsuc2  8757  nfixp1  8976  nneneq  9272  nneneqOLD  9284  scottex  9954  dfac2b  10200  infpssrlem4  10375  hsmexlem2  10496  hsmexlem4  10498  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  zorn2lem5  10569  konigthlem  10637  eltsk2g  10820  dedekind  11453  dedekindle  11454  lble  12247  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  fsuppmapnn0fiubex  14043  prodeq2ii  15959  fprodle  16044  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  mreiincl  17654  mreexexd  17706  catpropd  17767  acsmapd  18624  gsummatr01lem4  22685  cpmatmcllem  22745  alexsubALTlem3  24078  isucn2  24309  nosupbnd1  27777  noinfbnd1  27792  mptelee  28928  chirred  32427  opreu2reuALT  32505  foresf1o  32532  abrexss  32540  iinabrex  32591  aciunf1lem  32680  nn0min  32824  fprodex01  32829  isarchiofld  33312  elrspunidl  33421  reff  33785  locfinreflem  33786  cmpcref  33796  zarcmplem  33827  esumcl  33994  measvunilem  34176  measvunilem0  34177  measvuni  34178  voliune  34193  volfiniune  34194  omssubadd  34265  bnj1366  34805  bnj1379  34806  bnj571  34882  bnj1039  34947  bnj1128  34966  bnj1204  34988  bnj1279  34994  bnj1307  34999  bnj1388  35009  bnj1398  35010  bnj1444  35019  bnj1489  35032  bnj1525  35045  dfon2lem3  35749  domalom  37370  ralssiun  37373  fvineqsneu  37377  fvineqsneq  37378  heicant  37615  cover2  37675  upixp  37689  indexdom  37694  filbcmb  37700  riotasvd  38912  riotasv2d  38913  riotasv2s  38914  glbconxN  39335  pmapglbx  39726  pmapglb2xN  39729  cdleme26ee  40317  cdlemefr29exN  40359  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme41sn3a  40390  cdleme32d  40401  cdleme32f  40403  cdleme40m  40424  cdleme40n  40425  cdlemk36  40870  cdlemk38  40872  cdlemkid  40893  cdlemk19x  40900  cdlemk11t  40903  mzpexpmpt  42701  nadd1suc  43354  gneispace  44096  mnuprdlem4  44244  ssralv2  44502  tratrb  44507  fnchoice  44929  rfcnnnub  44936  uzwo4  44955  ralimralim  44983  suprnmpt  45081  choicefi  45107  axccdom  45129  axccd  45136  rnmptlb  45152  rnmptbddlem  45153  rnmptbd2lem  45157  rnmptbdlem  45164  upbdrech  45220  ssfiunibd  45224  iuneqfzuzlem  45249  infxrunb2  45283  xrralrecnnle  45298  supxrunb3  45314  supxrleubrnmpt  45321  unb2ltle  45330  rexabslelem  45333  allbutfiinf  45335  suprleubrnmpt  45337  uzub  45346  infxrgelbrnmpt  45369  cvgcaule  45407  mccl  45519  climsuse  45529  mullimc  45537  islptre  45540  mullimcf  45544  limcrecl  45550  islpcn  45560  limsupre  45562  limcleqr  45565  addlimc  45569  0ellimcdiv  45570  limclner  45572  climinf2lem  45627  limsupubuz  45634  climinf3  45637  limsupmnflem  45641  limsupmnfuzlem  45647  limsupre3uzlem  45656  climisp  45667  climrescn  45669  climxrrelem  45670  climxrre  45671  xlimmnfv  45755  xlimpnfv  45759  climxlim2lem  45766  cncfioobd  45818  stoweidlem16  45937  stoweidlem28  45949  stoweidlem29  45950  stoweidlem31  45952  stoweidlem35  45956  stoweidlem48  45969  stoweidlem51  45972  stoweidlem52  45973  stoweidlem53  45974  stoweidlem54  45975  stoweidlem56  45977  stoweidlem57  45978  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  wallispilem3  45988  stirlinglem13  46007  fourierdlem31  46059  fourierdlem39  46067  fourierdlem68  46095  fourierdlem71  46098  fourierdlem73  46100  fourierdlem77  46104  fourierdlem83  46110  fourierdlem87  46114  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  salexct  46255  subsaliuncl  46279  sge0lefi  46319  sge0isum  46348  sge0reuzb  46369  iundjiun  46381  voliunsge0lem  46393  meaiuninc3v  46405  ovnsubaddlem2  46492  hoiqssbllem3  46545  vonioo  46603  vonicc  46606  preimageiingt  46641  preimaleiinlt  46642  issmfle  46666  issmfgt  46677  issmfge  46691  smflimlem2  46693  smfsupmpt  46736  smfinflem  46738  smfinfmpt  46740  smfliminflem  46751  fsupdm  46763  finfdm  46767  ffnafv  47086  iccelpart  47307  sprsymrelfo  47371  mogoldbb  47659  sbgoldbo  47661  iunord  48768  setrec1lem2  48780  pgind  48809  aacllem  48895