Theorem nfa1 2196

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

Assertion

Ref	Expression
nfa1	⊢ Ⅎ𝑥∀𝑥𝜑

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1910	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2		nfe1 2195	. . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑
3	2	nfn 1944	. 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑
4	1, 3	nfxfr 1938	1 ⊢ Ⅎ𝑥∀𝑥𝜑

Syntax hints:  ¬ wn 3  ∀wal 1635  ∃wex 1859  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-10 2186

This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864

This theorem is referenced by:  nfna1  2197  nfia1  2198  nfnf1  2199  nfa2  2208  sb56  2284  nfs1v  2288  nf5  2293  axc4i  2309  hba1  2329  nfnf1OLD  2337  axc16nfOLD  2339  19.12  2340  nfa2OLD  2344  equs5aALT  2353  equs5eALT  2354  cbv1h  2443  axc15  2473  dral1  2489  nfald2  2495  equs5a  2508  equs5e  2509  equs5  2511  axc14  2533  sbf2  2543  nfsb4t  2550  sbcom3  2572  exsb  2631  nfmo1  2639  nfeu1  2653  moexex  2716  2eu6  2733  exists2  2737  nfaba1  2965  nfra1  3140  ceqsalgALT  3436  elrab3t  3569  csbie2t  3768  sbcnestgf  4203  dfnfc2  4661  mpteq12f  4936  axrep2  4980  axrep3  4981  axrep4  4982  alxfr  5089  copsex2t  5159  mosubopt  5178  fv3  6435  fvmptt  6530  fnoprabg  7000  pssnn  8426  fiint  8485  aceq1  9232  zorn2lem4  9615  zfcndrep  9730  mreexexd  16532  dfon2lem7  32035  bj-alalbial  33028  bj-exalbial  33029  bj-biexal1  33032  bj-bialal  33035  bj-cbv1hv  33065  bj-dral1v  33083  bj-axrep2  33121  bj-axrep3  33122  bj-axrep4  33123  ax11-pm  33150  bj-mo3OLD  33163  bj-snsetex  33279  exlimim  33524  exellim  33526  wl-nfimf1  33645  wl-nfae1  33647  wl-sb8t  33666  wl-sbnf1  33669  wl-lem-moexsb  33682  wl-mo2tf  33685  wl-eutf  33687  wl-mo2t  33689  wl-mo3t  33690  wl-sb8eut  33691  wl-ax11-lem3  33696  sbali  34244  nfbii2OLD  34295  setindtr  38109  axc11next  39123  iotain  39134  pm14.122b  39140  pm14.123b  39143  eubi  39153  ax6e2ndeqVD  39656  e2ebindALT  39676  ax6e2ndeqALT  39678  rexsb  41698