Theorem nfa1 2015

Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1701 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2034. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1743	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2014	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1768	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1771	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfna1  2016  nfia1  2017  nfnf1  2018  nfa2  2027  nf5  2102  axc4i  2116  sb56  2136  hba1  2137  nfnf1OLD  2145  axc16nfOLD  2149  19.12  2150  nfa2OLD  2154  equs5aALT  2165  equs5eALT  2166  cbv1h  2256  axc15  2291  dral1  2313  nfald2  2319  ax12v2OLD  2330  equs5a  2336  equs5e  2337  equs5  2339  axc14  2360  sbf2  2370  nfsb4t  2377  sbcom3  2399  exsb  2456  nfeu1  2468  moexex  2529  2eu6  2546  exists2  2550  nfaba1  2756  nfra1  2925  ceqsalgALT  3204  elrab3t  3330  csbie2t  3528  sbcnestgf  3947  dfnfc2  4390  dfnfc2OLD  4391  mpteq12f  4661  axrep2  4701  axrep3  4702  axrep4  4703  alxfr  4804  copsex2t  4883  mosubopt  4897  fv3  6116  fvmptt  6208  fnoprabg  6659  pssnn  8063  fiint  8122  aceq1  8823  zorn2lem4  9204  zfcndrep  9315  mreexexd  16131  mreexexdOLD  16132  dfon2lem7  30938  bj-alalbial  31879  bj-exalbial  31880  bj-biexal1  31883  bj-bialal  31886  bj-cbv1hv  31917  bj-dral1v  31936  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  ax11-pm  32007  bj-mo3OLD  32022  bj-snsetex  32144  bj-xnex  32245  exlimim  32365  exellim  32368  wl-nfimf1  32492  wl-nfae1  32494  wl-sb8t  32512  wl-sbnf1  32515  wl-lem-moexsb  32529  wl-mo2tf  32532  wl-eutf  32534  wl-mo2t  32536  wl-mo3t  32537  wl-sb8eut  32538  wl-ax11-lem3  32543  wl-sbcom3  32551  sbali  33085  nfbii2  33137  setindtr  36609  axc11next  37629  iotain  37640  pm14.122b  37646  pm14.123b  37649  eubi  37659  ax6e2ndeqVD  38167  e2ebindALT  38187  ax6e2ndeqALT  38189  rexsb  39817