Theorem nfal 1600

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 1534. (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 1485	. . . . . 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 1479	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1472	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1471	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1472	. . . . . 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 1479	. . . 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 1485	. . 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 1475	1 |- F/ x A. y ph

Syntax hints:   -> wi 4   A.wal 1371   F/wnf 1484

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 1471  ax-7 1472  ax-gen 1473

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

This theorem is referenced by:  nfnf  1601  nfa2  1603  aaan  1611  cbv3  1766  cbv2  1773  nfald  1784  cbval2  1946  nfsb4t  2043  nfeuv  2073  mo23  2097  bm1.1  2192  nfnfc1  2353  nfnfc  2357  nfeq  2358  nfabdw  2369  sbcnestgf  3153  dfnfc2  3882  nfdisjv  4047  nfdisj1  4048  nffr  4414  uchoice  6246  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidunben  12912  bdsepnft  16022  bdsepnfALT  16024  setindft  16100  strcollnft  16119  pw1nct  16142