Theorem nfal 1569

Description: If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1503. (Revised by Gino Giotto, 25-Aug-2024.)

Hypothesis

Ref	Expression
nfal.1	|- F/ x ph

Assertion

Ref	Expression
nfal	|- F/ x A. y ph

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		df-nf 1454	. . . . . 6 |- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2	1	biimpi 119	. . . . 5 |- ( F/ x ph -> A. x ( ph -> A. x ph ) )
3	2	alimi 1448	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1441	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1440	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1441	. . . . . 6 |- ( A. y A. x ph -> A. x A. y ph )
7	5, 6	syl6 33	. . . . 5 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. x A. y ph ) )
8	7	alimi 1448	. . . 4 |- ( A. x A. y ( ph -> A. x ph ) -> A. x ( A. y ph -> A. x A. y ph ) )
9	3, 4, 8	3syl 17	. . 3 |- ( A. y F/ x ph -> A. x ( A. y ph -> A. x A. y ph ) )
10		df-nf 1454	. . 3 |- ( F/ x A. y ph <-> A. x ( A. y ph -> A. x A. y ph ) )
11	9, 10	sylibr 133	. 2 |- ( A. y F/ x ph -> F/ x A. y ph )
12		nfal.1	. 2 |- F/ x ph
13	11, 12	mpg 1444	1 |- F/ x A. y ph

Syntax hints:   -> wi 4   A.wal 1346   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442

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

This theorem is referenced by:  nfnf  1570  nfa2  1572  aaan  1580  cbv3  1735  cbv2  1742  nfald  1753  cbval2  1914  nfsb4t  2007  nfeuv  2037  mo23  2060  bm1.1  2155  nfnfc1  2315  nfnfc  2319  nfeq  2320  nfabdw  2331  sbcnestgf  3100  dfnfc2  3814  nfdisjv  3978  nfdisj1  3979  nffr  4334  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidunben  12381  bdsepnft  13922  bdsepnfALT  13924  setindft  14000  strcollnft  14019  pw1nct  14036