Theorem nfal 1599

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 1533. (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 1484	. . . . . 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 1478	. . . 4 |- ( A. y F/ x ph -> A. y A. x ( ph -> A. x ph ) )
4		ax-7 1471	. . . 4 |- ( A. y A. x ( ph -> A. x ph ) -> A. x A. y ( ph -> A. x ph ) )
5		ax-5 1470	. . . . . 6 |- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. y A. x ph ) )
6		ax-7 1471	. . . . . 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 1478	. . . 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 1484	. . 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 1474	1 |- F/ x A. y ph

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

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

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

This theorem is referenced by:  nfnf  1600  nfa2  1602  aaan  1610  cbv3  1765  cbv2  1772  nfald  1783  cbval2  1945  nfsb4t  2042  nfeuv  2072  mo23  2095  bm1.1  2190  nfnfc1  2351  nfnfc  2355  nfeq  2356  nfabdw  2367  sbcnestgf  3145  dfnfc2  3868  nfdisjv  4033  nfdisj1  4034  nffr  4396  uchoice  6223  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidunben  12797  bdsepnft  15827  bdsepnfALT  15829  setindft  15905  strcollnft  15924  pw1nct  15944