Theorem spsbbi

Description: Biconditional property for substitution. Closed form of sbbii . Specialization of biconditional. (Contributed by NM, 2-Jun-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
2	1	alimi	|- ( A. x ( ph <-> ps ) -> A. x ( ph -> ps ) )
3		spsbim	|- ( A. x ( ph -> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )
4	2 3	syl	|- ( A. x ( ph <-> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )
5		biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )
6	5	alimi	|- ( A. x ( ph <-> ps ) -> A. x ( ps -> ph ) )
7		spsbim	|- ( A. x ( ps -> ph ) -> ( [ t / x ] ps -> [ t / x ] ph ) )
8	6 7	syl	|- ( A. x ( ph <-> ps ) -> ( [ t / x ] ps -> [ t / x ] ph ) )
9	4 8	impbid	|- ( A. x ( ph <-> ps ) -> ( [ t / x ] ph <-> [ t / x ] ps ) )