Theorem nfa1 1552

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

Syntax hints:   A.wal 1362   F/wnf 1471

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 1460  ax-ial 1545

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

This theorem is referenced by:  axc4i  1553  nfnf1  1555  nfa2  1590  nfia1  1591  alexdc  1630  nf2  1679  cbv1h  1757  sbf2  1789  sb4or  1844  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  sbalyz  2015  dvelimALT  2026  hbe1a  2039  nfeu1  2053  moim  2106  euexex  2127  nfaba1  2342  nfabdw  2355  nfra1  2525  ceqsalg  2788  elrab3t  2916  mo2icl  2940  csbie2t  3130  sbcnestgf  3133  dfss4st  3393  dfnfc2  3854  mpteq12f  4110  copsex2t  4275  ssopab2  4307  alxfr  4493  eunex  4594  mosubopt  4725  fv3  5578  fvmptt  5650  fnoprabg  6020  fiintim  6987  bj-exlimmp  15331  bdsepnft  15449  setindft  15527  strcollnft  15546