Theorem nfa1 1954

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

Syntax hints:   A.wal 1435   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664

This theorem is referenced by:  axc4i  1955  nfnf1  1956  nfna1  1960  axc16nf  2002  19.12  2008  nfa2  2011  nfia1  2012  nf2  2018  equs5a  2035  equs5e  2036  cbv1h  2074  dral1  2123  nfald2  2129  ax12v2  2139  equs5  2146  axc14  2167  sbf2  2177  nfsb4t  2184  sbcom3  2206  sb56  2224  exsb  2264  nfeu1  2278  moexex  2341  2eu1OLD  2355  2eu4OLD  2359  2eu6  2361  exists2  2367  nfaba1  2596  nfra1  2813  ceqsalgALT  3113  elrab3t  3234  csbie2t  3430  sbcnestgf  3818  dfnfc2  4240  mpteq12f  4502  axrep2  4540  axrep3  4541  axrep4  4542  alxfr  4635  copsex2t  4708  mosubopt  4719  fv3  5894  fvmptt  5981  fnoprabg  6411  pssnn  7796  fiint  7854  aceq1  8546  zorn2lem4  8927  zfcndrep  9038  mreexexd  15505  dfon2lem7  30222  bj-alalbial  31035  bj-exalbial  31036  bj-biexal1  31039  bj-bialal  31042  bj-cbv1hv  31073  bj-axc16nf  31104  bj-dral1v  31106  bj-axc15v  31110  bj-equs5v  31112  bj-sb56  31129  bj-axrep2  31155  bj-axrep3  31156  bj-axrep4  31157  ax11-pm  31185  bj-mo3OLD  31198  bj-snsetex  31306  exlimim  31478  exellim  31481  wl-nfimf1  31565  wl-nfae1  31567  wl-sb8t  31587  wl-sbnf1  31590  wl-lem-moexsb  31604  wl-mo2tf  31607  wl-mo2t  31608  wl-mo3t  31609  wl-sb8eut  31610  wl-ax12v3  31616  wl-ax11-lem3  31621  wl-sbcom3  31629  sbali  32054  nfbii2  32106  setindtr  35585  axc11next  36394  iotain  36405  pm14.122b  36411  pm14.123b  36414  eubi  36424  ax6e2ndeqVD  36946  e2ebindALT  36966  ax6e2ndeqALT  36968  rexsb  37980