Theorem nfsb4t

Description: A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 ). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	nfsb4t	|- ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
2	1	sps	|- ( A. x x = y -> ( ph <-> [ y / x ] ph ) )
3	2	drnf2	|- ( A. x x = y -> ( F/ z ph <-> F/ z [ y / x ] ph ) )
4	3	biimpd	|- ( A. x x = y -> ( F/ z ph -> F/ z [ y / x ] ph ) )
5	4	spsd	|- ( A. x x = y -> ( A. x F/ z ph -> F/ z [ y / x ] ph ) )
6	5	impcom	|- ( ( A. x F/ z ph /\ A. x x = y ) -> F/ z [ y / x ] ph )
7	6	a1d	|- ( ( A. x F/ z ph /\ A. x x = y ) -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
8		nfnf1	|- F/ z F/ z ph
9	8	nfal	|- F/ z A. x F/ z ph
10		nfnae	|- F/ z -. A. x x = y
11	9 10	nfan	|- F/ z ( A. x F/ z ph /\ -. A. x x = y )
12		nfa1	|- F/ x A. x F/ z ph
13		nfnae	|- F/ x -. A. x x = y
14	12 13	nfan	|- F/ x ( A. x F/ z ph /\ -. A. x x = y )
15		sp	|- ( A. x F/ z ph -> F/ z ph )
16	15	adantr	|- ( ( A. x F/ z ph /\ -. A. x x = y ) -> F/ z ph )
17		nfsb2	|- ( -. A. x x = y -> F/ x [ y / x ] ph )
18	17	adantl	|- ( ( A. x F/ z ph /\ -. A. x x = y ) -> F/ x [ y / x ] ph )
19	1	a1i	|- ( ( A. x F/ z ph /\ -. A. x x = y ) -> ( x = y -> ( ph <-> [ y / x ] ph ) ) )
20	11 14 16 18 19	dvelimdf	|- ( ( A. x F/ z ph /\ -. A. x x = y ) -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
21	7 20	pm2.61dan	|- ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )