Theorem nfa1 1883

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

Syntax hints:   A.wal 1381   F/wnf 1603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840

This theorem depends on definitions:  df-bi 185  df-ex 1600  df-nf 1604

This theorem is referenced by:  axc4i  1884  nfnf1  1885  nfna1  1889  ax16nf  1930  19.12  1936  nfa2  1939  nfia1  1940  nf2  1946  equs5a  1964  equs5e  1965  cbv1h  2004  dral1  2053  nfald2  2059  ax12v2  2069  equs5  2078  axc14  2099  sbf2  2109  nfsb4t  2116  sbcom3  2139  sb56  2158  exsb  2198  nfeu1  2280  mo3OLD  2310  moexex  2349  2eu1OLD  2363  2eu4OLD  2367  2eu6  2369  exists2  2375  nfaba1  2610  nfra1  2824  ceqsalgALT  3121  elrab3t  3242  csbie2t  3449  sbcnestgf  3825  dfnfc2  4252  mpteq12f  4513  axrep2  4550  axrep3  4551  axrep4  4552  alxfr  4650  copsex2t  4724  mosubopt  4735  fv3  5869  fvmptt  5956  fnoprabg  6388  pssnn  7740  fiint  7799  aceq1  8501  zorn2lem4  8882  axpowndlem3OLD  8979  zfcndrep  8995  mreexexd  14922  dfon2lem7  29196  wl-nfimf1  29953  wl-nfae1  29955  wl-sb8t  29975  wl-sbnf1  29978  wl-lem-moexsb  29992  wl-mo2t  29995  wl-mo3t  29996  wl-sb8eut  29997  wl-ax11-lem3  30002  wl-sbcom3  30010  sbali  30490  nfbii2  30542  setindtr  30941  axc11next  31267  iotain  31278  pm14.122b  31284  pm14.123b  31287  eubi  31297  rexsb  32011  ax6e2ndeqVD  33442  e2ebindALT  33462  ax6e2ndeqALT  33464  bj-alalbial  34003  bj-exalbial  34004  bj-biexal1  34007  bj-bialal  34010  bj-cbv1hv  34041  bj-ax16nf  34072  bj-dral1v  34074  bj-axc15v  34078  bj-equs5v  34080  bj-sb56  34097  bj-axrep2  34123  bj-axrep3  34124  bj-axrep4  34125  ax11-pm  34153  bj-snsetex  34269