Theorem nfra1 3145

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1783  df-nf 1787  df-ral 3070

This theorem is referenced by:  hbra1  3146  nfra2wOLDOLD  3157  nfra2  3158  r19.12  3258  r19.12OLD  3259  ralcom2  3291  ralimda  3432  2reu1  3831  nfss  3914  rspn0OLD  4288  ralidmOLD  4447  2reu4lem  4457  iuneqconst  4936  nfii1  4960  dfiun2gOLD  4962  mpteq12f  5163  reusv1  5321  reusv2lem1  5322  reusv2lem2  5323  reusv2lem3  5324  ralxfrALT  5339  fvmptss  6896  ffnfv  7001  riota5f  7270  mpoeq123  7356  tfinds  7715  peano5OLD  7750  zfrep6  7806  frrlem4  8114  wfrlem4OLD  8152  tfr3  8239  tz7.48-1  8283  tz7.49  8285  nfixp1  8715  nneneq  9001  nneneqOLD  9013  scottex  9652  dfac2b  9895  infpssrlem4  10071  hsmexlem2  10192  hsmexlem4  10194  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  zorn2lem5  10265  konigthlem  10333  eltsk2g  10516  dedekind  11147  dedekindle  11148  lble  11936  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  fsuppmapnn0fiubex  13721  prodeq2ii  15632  fprodle  15715  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  mreiincl  17314  mreexexd  17366  catpropd  17427  acsmapd  18281  gsummatr01lem4  21816  cpmatmcllem  21876  alexsubALTlem3  23209  isucn2  23440  mptelee  27272  chirred  30766  opreu2reuALT  30834  foresf1o  30859  abrexss  30866  iinabrex  30917  aciunf1lem  31008  nn0min  31143  fprodex01  31148  isarchiofld  31525  elrspunidl  31615  reff  31798  locfinreflem  31799  cmpcref  31809  zarcmplem  31840  esumcl  32007  measvunilem  32189  measvunilem0  32190  measvuni  32191  voliune  32206  volfiniune  32207  omssubadd  32276  bnj1366  32818  bnj1379  32819  bnj571  32895  bnj1039  32960  bnj1128  32979  bnj1204  33001  bnj1279  33007  bnj1307  33012  bnj1388  33022  bnj1398  33023  bnj1444  33032  bnj1489  33045  bnj1525  33058  dfon2lem3  33770  nosupbnd1  33926  noinfbnd1  33941  domalom  35584  ralssiun  35587  fvineqsneu  35591  fvineqsneq  35592  heicant  35821  cover2  35881  upixp  35896  indexdom  35901  filbcmb  35907  riotasvd  36977  riotasv2d  36978  riotasv2s  36979  glbconxN  37399  pmapglbx  37790  pmapglb2xN  37793  cdleme26ee  38381  cdlemefr29exN  38423  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32d  38465  cdleme32f  38467  cdleme40m  38488  cdleme40n  38489  cdlemk36  38934  cdlemk38  38936  cdlemkid  38957  cdlemk19x  38964  cdlemk11t  38967  mzpexpmpt  40574  gneispace  41751  mnuprdlem4  41900  ssralv2  42158  tratrb  42163  fnchoice  42579  rfcnnnub  42586  uzwo4  42608  ralimralim  42638  suprnmpt  42717  fompt  42737  choicefi  42747  axccdom  42769  axccd  42775  rnmptlb  42795  rnmptbddlem  42796  rnmptbd2lem  42801  rnmptbdlem  42808  upbdrech  42851  ssfiunibd  42855  iuneqfzuzlem  42880  infxrunb2  42914  xrralrecnnle  42929  supxrunb3  42946  supxrleubrnmpt  42953  unb2ltle  42962  rexabslelem  42965  allbutfiinf  42967  suprleubrnmpt  42969  uzub  42978  infxrgelbrnmpt  43001  mccl  43146  climsuse  43156  mullimc  43164  islptre  43167  mullimcf  43171  limcrecl  43177  islpcn  43187  limsupre  43189  limcleqr  43192  addlimc  43196  0ellimcdiv  43197  limclner  43199  climinf2lem  43254  limsupubuz  43261  climinf3  43264  limsupmnflem  43268  limsupmnfuzlem  43274  limsupre3uzlem  43283  climisp  43294  climrescn  43296  climxrrelem  43297  climxrre  43298  xlimmnfv  43382  xlimpnfv  43386  climxlim2lem  43393  cncfioobd  43445  stoweidlem16  43564  stoweidlem28  43576  stoweidlem29  43577  stoweidlem31  43579  stoweidlem35  43583  stoweidlem48  43596  stoweidlem51  43599  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  stoweidlem56  43604  stoweidlem57  43605  stoweidlem59  43607  stoweidlem60  43608  stoweidlem62  43610  wallispilem3  43615  stirlinglem13  43634  fourierdlem31  43686  fourierdlem39  43694  fourierdlem68  43722  fourierdlem71  43725  fourierdlem73  43727  fourierdlem77  43731  fourierdlem83  43737  fourierdlem87  43741  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem113  43767  salexct  43880  subsaliuncl  43904  sge0lefi  43943  sge0isum  43972  sge0reuzb  43993  iundjiun  44005  voliunsge0lem  44017  meaiuninc3v  44029  ovnsubaddlem2  44116  hoiqssbllem3  44169  vonioo  44227  vonicc  44230  preimageiingt  44265  preimaleiinlt  44266  issmfle  44290  issmfgt  44301  issmfge  44315  smflimlem2  44317  smfsupmpt  44359  smfinflem  44361  smfinfmpt  44363  smfliminflem  44374  ffnafv  44674  iccelpart  44896  sprsymrelfo  44960  mogoldbb  45248  sbgoldbo  45250  iunord  46393  setrec1lem2  46405  aacllem  46516