Theorem nfa1 1486

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

Syntax hints:   A.wal 1294   F/wnf 1401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1390  ax-ial 1479

This theorem depends on definitions:  df-bi 116  df-nf 1402

This theorem is referenced by:  nfnf1  1488  nfa2  1523  nfia1  1524  alexdc  1562  nf2  1610  cbv1h  1687  sbf2  1715  sb4or  1768  nfsbxy  1873  nfsbxyt  1874  sbcomxyyz  1901  sbalyz  1930  dvelimALT  1941  nfeu1  1966  moim  2019  euexex  2040  nfaba1  2241  nfra1  2420  ceqsalg  2661  elrab3t  2784  mo2icl  2808  csbie2t  2990  sbcnestgf  2993  dfss4st  3248  dfnfc2  3693  mpteq12f  3940  copsex2t  4096  ssopab2  4126  alxfr  4311  eunex  4405  mosubopt  4532  fv3  5363  fvmptt  5430  fnoprabg  5784  fiintim  6719  bj-exlimmp  12378  bdsepnft  12486  setindft  12568  strcollnft  12587