Theorem nfal 1625

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 1559. (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 1510	. . . . . 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 1504	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1497	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1496	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1497	. . . . . 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 1504	. . . 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 1510	. . 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 1500	1 |- F/ x A. y ph

Syntax hints:   -> wi 4   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-5 1496  ax-7 1497  ax-gen 1498

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

This theorem is referenced by:  nfnf  1626  nfa2  1628  aaan  1636  cbv3  1790  cbv2  1797  nfald  1808  cbval2  1970  nfsb4t  2067  nfeuv  2097  mo23  2121  bm1.1  2216  nfnfc1  2378  nfnfc  2382  nfeq  2383  nfabdw  2394  sbcnestgf  3180  dfnfc2  3916  nfdisjv  4081  nfdisj1  4082  nffr  4452  uchoice  6309  modom  7037  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidunben  13127  bdsepnft  16603  bdsepnfALT  16605  setindft  16681  strcollnft  16700  pw1nct  16725