Theorem nfa1 1589

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

Syntax hints:   A.wal 1395   F/wnf 1508

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 1497  ax-ial 1582

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

This theorem is referenced by:  axc4i  1590  nfnf1  1592  nfa2  1627  nfia1  1628  alexdc  1667  nf2  1716  cbv1h  1794  sbf2  1826  sb4or  1881  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  sbalyz  2052  dvelimALT  2063  hbe1a  2076  nfeu1  2090  moim  2144  euexex  2165  nfaba1  2380  nfabdw  2393  nfra1  2563  ceqsalg  2831  elrab3t  2961  mo2icl  2985  csbie2t  3176  sbcnestgf  3179  dfss4st  3440  dfnfc2  3911  mpteq12f  4169  copsex2t  4337  ssopab2  4370  alxfr  4558  eunex  4659  mosubopt  4791  fv3  5662  fvmptt  5738  fnoprabg  6121  fiintim  7122  bj-exlimmp  16365  bdsepnft  16482  setindft  16560  strcollnft  16579