Theorem nfal 1624

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 1558. (Revised by GG, 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 1509	. . . . . 6 |- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2	1	biimpi 120	. . . . 5 |- ( F/ x ph -> A. x ( ph -> A. x ph ) )
3	2	alimi 1503	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1496	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1495	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1496	. . . . . 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 1503	. . . 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 1509	. . 3 |- ( F/ x A. y ph <-> A. x ( A. y ph -> A. x A. y ph ) )
11	9, 10	sylibr 134	. 2 |- ( A. y F/ x ph -> F/ x A. y ph )
12		nfal.1	. 2 |- F/ x ph
13	11, 12	mpg 1499	1 |- F/ x A. y ph

Syntax hints:   -> wi 4   A.wal 1395   F/wnf 1508

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-5 1495  ax-7 1496  ax-gen 1497

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

This theorem is referenced by:  nfnf  1625  nfa2  1627  aaan  1635  cbv3  1790  cbv2  1797  nfald  1808  cbval2  1970  nfsb4t  2067  nfeuv  2097  mo23  2121  bm1.1  2216  nfnfc1  2377  nfnfc  2381  nfeq  2382  nfabdw  2393  sbcnestgf  3179  dfnfc2  3911  nfdisjv  4076  nfdisj1  4077  nffr  4446  uchoice  6300  modom  6994  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidunben  13065  bdsepnft  16533  bdsepnfALT  16535  setindft  16611  strcollnft  16630  pw1nct  16655