Theorem sb4bOLD

Description: Obsolete version of sb4b as of 21-Feb-2024. (Contributed by NM, 27-May-1997) Revise df-sb . (Revised by Wolf Lammen, 25-Jul-2023) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sb4bOLD	|- ( -. A. x x = t -> ( [ t / x ] ph <-> A. x ( x = t -> ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfeqf2	|- ( -. A. x x = t -> F/ x y = t )
2		nfnf1	|- F/ x F/ x y = t
3		id	|- ( F/ x y = t -> F/ x y = t )
4	2 3	nfan1	|- F/ x ( F/ x y = t /\ y = t )
5		equequ2	|- ( y = t -> ( x = y <-> x = t ) )
6	5	imbi1d	|- ( y = t -> ( ( x = y -> ph ) <-> ( x = t -> ph ) ) )
7	6	adantl	|- ( ( F/ x y = t /\ y = t ) -> ( ( x = y -> ph ) <-> ( x = t -> ph ) ) )
8	4 7	albid	|- ( ( F/ x y = t /\ y = t ) -> ( A. x ( x = y -> ph ) <-> A. x ( x = t -> ph ) ) )
9	8	pm5.74da	|- ( F/ x y = t -> ( ( y = t -> A. x ( x = y -> ph ) ) <-> ( y = t -> A. x ( x = t -> ph ) ) ) )
10	1 9	syl	|- ( -. A. x x = t -> ( ( y = t -> A. x ( x = y -> ph ) ) <-> ( y = t -> A. x ( x = t -> ph ) ) ) )
11	10	albidv	|- ( -. A. x x = t -> ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. y ( y = t -> A. x ( x = t -> ph ) ) ) )
12		df-sb	|- ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
13		ax6ev	|- E. y y = t
14	13	a1bi	|- ( A. x ( x = t -> ph ) <-> ( E. y y = t -> A. x ( x = t -> ph ) ) )
15		19.23v	|- ( A. y ( y = t -> A. x ( x = t -> ph ) ) <-> ( E. y y = t -> A. x ( x = t -> ph ) ) )
16	14 15	bitr4i	|- ( A. x ( x = t -> ph ) <-> A. y ( y = t -> A. x ( x = t -> ph ) ) )
17	11 12 16	3bitr4g	|- ( -. A. x x = t -> ( [ t / x ] ph <-> A. x ( x = t -> ph ) ) )