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

This proof depends on syntax axioms:   A.wal 1400   F/wnf 1513

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used 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  3953  mpteq12f  4212  copsex2t  4387  ssopab2  4420  alxfr  4609  eunex  4710  mosubopt  4842  fv3  5721  fvmptt  5800  fnoprabg  6192  fiintim  7242  bj-exlimmp  17002  bdsepnft  17118  setindft  17196  strcollnft  17215  dfalseu2  17384