Theorem nfa1 1956

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 1955	. 2 |- ( A. x ph -> A. x A. x ph )
2	1	nfi 1668	1 |- F/ x A. x ph

Syntax hints:   A.wal 1435   F/wnf 1661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909

This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662

This theorem is referenced by:  axc4i  1957  nfnf1  1958  nfna1  1962  axc16nf  2004  19.12  2010  nfa2  2013  nfia1  2014  nf2  2018  equs5a  2043  equs5e  2044  cbv1h  2083  dral1  2133  nfald2  2139  ax12v2  2149  equs5  2156  axc14  2177  sbf2  2187  nfsb4t  2194  sbcom3  2216  sb56  2234  exsb  2274  nfeu1  2286  moexex  2347  2eu6  2364  exists2  2368  nfaba1  2574  nfra1  2746  ceqsalgALT  3049  elrab3t  3170  csbie2t  3367  sbcnestgf  3757  dfnfc2  4180  mpteq12f  4443  axrep2  4481  axrep3  4482  axrep4  4483  alxfr  4577  copsex2t  4650  mosubopt  4661  fv3  5838  fvmptt  5925  fnoprabg  6355  pssnn  7743  fiint  7801  aceq1  8499  zorn2lem4  8880  zfcndrep  8990  mreexexd  15497  dfon2lem7  30386  bj-alalbial  31201  bj-exalbial  31202  bj-biexal1  31205  bj-bialal  31208  bj-cbv1hv  31236  bj-axc16nf  31264  bj-dral1v  31266  bj-axc15v  31270  bj-equs5v  31272  bj-sb56  31289  bj-axrep2  31315  bj-axrep3  31316  bj-axrep4  31317  ax11-pm  31345  bj-mo3OLD  31358  bj-snsetex  31468  exlimim  31651  exellim  31654  wl-nfimf1  31765  wl-nfae1  31767  wl-sb8t  31787  wl-sbnf1  31790  wl-lem-moexsb  31804  wl-mo2tf  31807  wl-eutf  31809  wl-mo2t  31811  wl-mo3t  31812  wl-sb8eut  31813  wl-ax12v3  31819  wl-ax11-lem3  31824  wl-sbcom3  31832  sbali  32257  nfbii2  32309  setindtr  35792  axc11next  36670  iotain  36681  pm14.122b  36687  pm14.123b  36690  eubi  36700  ax6e2ndeqVD  37222  e2ebindALT  37242  ax6e2ndeqALT  37244  rexsb  38403