Theorem nfa1 1564

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

Syntax hints:   A.wal 1371   F/wnf 1483

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 1472  ax-ial 1557

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

This theorem is referenced by:  axc4i  1565  nfnf1  1567  nfa2  1602  nfia1  1603  alexdc  1642  nf2  1691  cbv1h  1769  sbf2  1801  sb4or  1856  nfsbxy  1970  nfsbxyt  1971  sbcomxyyz  2000  sbalyz  2027  dvelimALT  2038  hbe1a  2051  nfeu1  2065  moim  2118  euexex  2139  nfaba1  2354  nfabdw  2367  nfra1  2537  ceqsalg  2800  elrab3t  2928  mo2icl  2952  csbie2t  3142  sbcnestgf  3145  dfss4st  3406  dfnfc2  3868  mpteq12f  4124  copsex2t  4289  ssopab2  4322  alxfr  4508  eunex  4609  mosubopt  4740  fv3  5599  fvmptt  5671  fnoprabg  6046  fiintim  7028  bj-exlimmp  15705  bdsepnft  15823  setindft  15901  strcollnft  15920