Theorem nfa1 1990

Description: x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

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

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		hba1 1989	. 2 |- ( A. x ph -> A. x A. x ph )
2	1	nfi 1685	1 |- F/ x A. x ph

Syntax hints:   A.wal 1453   F/wnf 1678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679

This theorem is referenced by:  axc4i  1991  nfnf1  1992  nfna1  1996  axc16nf  2038  19.12  2044  nfa2  2047  nfia1  2048  nf2  2052  equs5a  2079  equs5e  2080  sb56  2092  cbv1h  2122  dral1  2170  nfald2  2176  ax12v2  2186  equs5  2193  axc14  2212  sbf2  2222  nfsb4t  2229  sbcom3  2251  exsb  2308  nfeu1  2320  moexex  2381  2eu6  2398  exists2  2402  nfaba1  2608  nfra1  2781  ceqsalgALT  3085  elrab3t  3207  csbie2t  3404  sbcnestgf  3796  dfnfc2  4230  mpteq12f  4493  axrep2  4531  axrep3  4532  axrep4  4533  alxfr  4627  copsex2t  4702  mosubopt  4713  fv3  5901  fvmptt  5988  fnoprabg  6424  pssnn  7816  fiint  7874  aceq1  8574  zorn2lem4  8955  zfcndrep  9065  mreexexd  15603  dfon2lem7  30484  bj-alalbial  31340  bj-exalbial  31341  bj-biexal1  31344  bj-bialal  31347  bj-cbv1hv  31376  bj-axc16nf  31401  bj-dral1v  31403  bj-axc15v  31407  bj-equs5v  31409  bj-axrep2  31449  bj-axrep3  31450  bj-axrep4  31451  ax11-pm  31479  bj-mo3OLD  31492  bj-snsetex  31602  exlimim  31789  exellim  31792  wl-nfimf1  31903  wl-nfae1  31905  wl-sb8t  31925  wl-sbnf1  31928  wl-lem-moexsb  31942  wl-mo2tf  31945  wl-eutf  31947  wl-mo2t  31949  wl-mo3t  31950  wl-sb8eut  31951  wl-ax12v3  31957  wl-ax11-lem3  31962  wl-sbcom3  31970  sbali  32395  nfbii2  32447  setindtr  35924  axc11next  36801  iotain  36812  pm14.122b  36818  pm14.123b  36821  eubi  36831  ax6e2ndeqVD  37346  e2ebindALT  37366  ax6e2ndeqALT  37368  rexsb  38627