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  1954  nfsbxyt  1955  sbcomxyyz  1984  sbalyz  2011  dvelimALT  2022  hbe1a  2035  nfeu1  2049  moim  2102  euexex  2123  nfaba1  2338  nfabdw  2351  nfra1  2521  ceqsalg  2780  elrab3t  2907  mo2icl  2931  csbie2t  3120  sbcnestgf  3123  dfss4st  3383  dfnfc2  3842  mpteq12f  4098  copsex2t  4263  ssopab2  4293  alxfr  4479  eunex  4578  mosubopt  4709  fv3  5557  fvmptt  5628  fnoprabg  5997  fiintim  6957  bj-exlimmp  14979  bdsepnft  15097  setindft  15175  strcollnft  15194