Theorem nfa1 1565

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

Syntax hints:   A.wal 1371   F/wnf 1484

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 1473  ax-ial 1558

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

This theorem is referenced by:  axc4i  1566  nfnf1  1568  nfa2  1603  nfia1  1604  alexdc  1643  nf2  1692  cbv1h  1770  sbf2  1802  sb4or  1857  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  sbalyz  2028  dvelimALT  2039  hbe1a  2052  nfeu1  2066  moim  2120  euexex  2141  nfaba1  2356  nfabdw  2369  nfra1  2539  ceqsalg  2805  elrab3t  2935  mo2icl  2959  csbie2t  3150  sbcnestgf  3153  dfss4st  3414  dfnfc2  3882  mpteq12f  4140  copsex2t  4307  ssopab2  4340  alxfr  4526  eunex  4627  mosubopt  4758  fv3  5622  fvmptt  5694  fnoprabg  6069  fiintim  7054  bj-exlimmp  15905  bdsepnft  16022  setindft  16100  strcollnft  16119