Theorem nfa1 1590

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

Syntax hints:   A.wal 1396   F/wnf 1509

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 1498  ax-ial 1583

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

This theorem is referenced by:  axc4i  1591  nfnf1  1593  nfa2  1628  nfia1  1629  alexdc  1668  nf2  1716  cbv1h  1795  sbf2  1827  sb4or  1882  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  sbalyz  2053  dvelimALT  2064  hbe1a  2077  nfeu1  2091  moim  2145  euexex  2166  nfaba1  2390  nfabdw  2403  nfra1  2573  ceqsalg  2842  elrab3t  2972  mo2icl  2996  csbie2t  3187  sbcnestgf  3190  dfss4st  3454  dfnfc2  3932  mpteq12f  4190  copsex2t  4361  ssopab2  4394  alxfr  4582  eunex  4683  mosubopt  4815  fv3  5693  fvmptt  5769  fnoprabg  6154  fiintim  7191  bj-exlimmp  16541  bdsepnft  16657  setindft  16735  strcollnft  16754