Theorem nfa1 1563

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

Syntax hints:   A.wal 1370   F/wnf 1482

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 1471  ax-ial 1556

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

This theorem is referenced by:  axc4i  1564  nfnf1  1566  nfa2  1601  nfia1  1602  alexdc  1641  nf2  1690  cbv1h  1768  sbf2  1800  sb4or  1855  nfsbxy  1969  nfsbxyt  1970  sbcomxyyz  1999  sbalyz  2026  dvelimALT  2037  hbe1a  2050  nfeu1  2064  moim  2117  euexex  2138  nfaba1  2353  nfabdw  2366  nfra1  2536  ceqsalg  2799  elrab3t  2927  mo2icl  2951  csbie2t  3141  sbcnestgf  3144  dfss4st  3405  dfnfc2  3867  mpteq12f  4123  copsex2t  4288  ssopab2  4321  alxfr  4507  eunex  4608  mosubopt  4739  fv3  5598  fvmptt  5670  fnoprabg  6045  fiintim  7027  bj-exlimmp  15667  bdsepnft  15785  setindft  15863  strcollnft  15882