Theorem nfa1 2028

Description: The setvar x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1710 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 12-Oct-2021.)

Assertion

Ref	Expression
nfa1	|- F/ x A. x ph

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		alex 1753	. 2 |- ( A. x ph <-> -. E. x -. ph )
2		nfe1 2027	. . 3 |- F/ x E. x -. ph
3	2	nfn 1784	. 2 |- F/ x -. E. x -. ph
4	1, 3	nfxfr 1779	1 |- F/ x A. x ph

Syntax hints:   -. wn 3   A.wal 1481   E.wex 1704   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfna1  2029  nfia1  2030  nfnf1  2031  nfa2  2040  nf5  2116  axc4i  2131  sb56  2150  hba1  2151  nfnf1OLD  2159  axc16nfOLD  2163  19.12  2164  nfa2OLD  2168  equs5aALT  2177  equs5eALT  2178  cbv1h  2268  axc15  2303  dral1  2325  nfald2  2331  ax12v2OLD  2342  equs5a  2348  equs5e  2349  equs5  2351  axc14  2372  sbf2  2382  nfsb4t  2389  sbcom3  2411  exsb  2468  nfeu1  2480  moexex  2541  2eu6  2558  exists2  2562  nfaba1  2770  nfra1  2941  ceqsalgALT  3231  elrab3t  3362  csbie2t  3562  sbcnestgf  3995  dfnfc2  4454  dfnfc2OLD  4455  mpteq12f  4731  axrep2  4773  axrep3  4774  axrep4  4775  alxfr  4878  copsex2t  4957  mosubopt  4972  fv3  6206  fvmptt  6300  fnoprabg  6761  pssnn  8178  fiint  8237  aceq1  8940  zorn2lem4  9321  zfcndrep  9436  mreexexd  16308  mreexexdOLD  16309  dfon2lem7  31694  bj-alalbial  32692  bj-exalbial  32693  bj-biexal1  32696  bj-bialal  32699  bj-cbv1hv  32730  bj-dral1v  32748  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  ax11-pm  32819  bj-mo3OLD  32832  bj-snsetex  32951  exlimim  33189  exellim  33192  wl-nfimf1  33313  wl-nfae1  33315  wl-sb8t  33333  wl-sbnf1  33336  wl-lem-moexsb  33350  wl-mo2tf  33353  wl-eutf  33355  wl-mo2t  33357  wl-mo3t  33358  wl-sb8eut  33359  wl-ax11-lem3  33364  wl-sbcom3  33372  sbali  33915  nfbii2  33967  setindtr  37591  axc11next  38607  iotain  38618  pm14.122b  38624  pm14.123b  38627  eubi  38637  ax6e2ndeqVD  39145  e2ebindALT  39165  ax6e2ndeqALT  39167  rexsb  41168