Theorem nfa1 1594

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

Syntax hints:   A.wal 1400   F/wnf 1513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514

This theorem is referenced by:  axc4i  1595  nfnf1  1597  nfa2  1632  nfia1  1633  alexdc  1672  nf2  1720  cbv1h  1799  sbf2  1831  sb4or  1886  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  sbalyz  2059  dvelimALT  2070  hbe1a  2083  nfeu1  2097  moim  2151  euexex  2172  nfaba1  2398  nfabdw  2411  nfra1  2581  ceqsalg  2850  elrab3t  2981  mo2icl  3005  csbie2t  3196  sbcnestgf  3199  dfss4st  3464  dfnfc2  3948  mpteq12f  4206  copsex2t  4380  ssopab2  4413  alxfr  4602  eunex  4703  mosubopt  4835  fv3  5713  fvmptt  5791  fnoprabg  6179  fiintim  7228  bj-exlimmp  16711  bdsepnft  16827  setindft  16905  strcollnft  16924