Theorem nfal 1553

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 1487. (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 1438	. . . . . 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 1432	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1425	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1424	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1425	. . . . . 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 1432	. . . 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 1438	. . 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 1428	1 |- F/ x A. y ph

Syntax hints:   -> wi 4   A.wal 1330   F/wnf 1437

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 1424  ax-7 1425  ax-gen 1426

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

This theorem is referenced by:  nfnf  1554  nfa2  1556  aaan  1564  cbv3  1719  cbv2  1726  nfald  1737  cbval2  1898  nfsb4t  1991  nfeuv  2021  mo23  2044  bm1.1  2139  nfnfc1  2299  nfnfc  2303  nfeq  2304  nfabdw  2315  sbcnestgf  3078  dfnfc2  3786  nfdisjv  3950  nfdisj1  3951  nffr  4304  exmidfodomrlemr  7116  exmidfodomrlemrALT  7117  exmidunben  12106  bdsepnft  13400  bdsepnfALT  13402  setindft  13478  strcollnft  13497  pw1nct  13514