Theorem nfa1 1902

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

Syntax hints:   A.wal 1396   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622

This theorem is referenced by:  axc4i  1903  nfnf1  1904  nfna1  1908  ax16nf  1949  19.12  1955  nfa2  1958  nfia1  1959  nf2  1965  equs5a  1983  equs5e  1984  cbv1h  2023  dral1  2071  nfald2  2077  ax12v2  2087  equs5  2094  axc14  2115  sbf2  2125  nfsb4t  2132  sbcom3  2155  sb56  2174  exsb  2214  nfeu1  2296  mo3OLD  2325  moexex  2360  2eu1OLD  2374  2eu4OLD  2378  2eu6  2380  exists2  2386  nfaba1  2621  nfra1  2835  ceqsalgALT  3132  elrab3t  3253  csbie2t  3449  sbcnestgf  3834  dfnfc2  4253  mpteq12f  4515  axrep2  4552  axrep3  4553  axrep4  4554  alxfr  4650  copsex2t  4723  mosubopt  4734  fv3  5861  fvmptt  5947  fnoprabg  6376  pssnn  7731  fiint  7789  aceq1  8489  zorn2lem4  8870  zfcndrep  8981  mreexexd  15137  dfon2lem7  29461  wl-nfimf1  30218  wl-nfae1  30220  wl-sb8t  30240  wl-sbnf1  30243  wl-lem-moexsb  30257  wl-mo2t  30260  wl-mo3t  30261  wl-sb8eut  30262  wl-ax11-lem3  30267  wl-sbcom3  30275  sbali  30755  nfbii2  30807  setindtr  31205  axc11next  31554  iotain  31565  pm14.122b  31571  pm14.123b  31574  eubi  31584  rexsb  32412  ax6e2ndeqVD  34110  e2ebindALT  34130  ax6e2ndeqALT  34132  bj-alalbial  34656  bj-exalbial  34657  bj-biexal1  34660  bj-bialal  34663  bj-cbv1hv  34694  bj-ax16nf  34725  bj-dral1v  34727  bj-axc15v  34731  bj-equs5v  34733  bj-sb56  34750  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778  ax11-pm  34806  bj-snsetex  34922