Theorem nfa1 1477

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

Syntax hints:   A.wal 1285   F/wnf 1392

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-ial 1470

This theorem depends on definitions:  df-bi 115  df-nf 1393

This theorem is referenced by:  nfnf1  1479  nfa2  1514  nfia1  1515  alexdc  1553  nf2  1601  cbv1h  1677  sbf2  1705  sb4or  1758  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  sbalyz  1920  dvelimALT  1931  nfeu1  1956  moim  2009  euexex  2030  nfaba1  2230  nfra1  2405  ceqsalg  2641  elrab3t  2761  mo2icl  2785  csbie2t  2965  sbcnestgf  2968  dfss4st  3221  dfnfc2  3654  mpteq12f  3893  copsex2t  4046  ssopab2  4076  alxfr  4257  eunex  4350  mosubopt  4471  fv3  5291  fvmptt  5357  fnoprabg  5703  bj-exlimmp  11115  bdsepnft  11223  setindft  11305  strcollnft  11324