Theorem sbciegft

Description: Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf .) (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016) (Proof shortened by SN, 14-May-2025)

	Ref	Expression
Assertion	sbciegft	|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbc6g	|- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
2	1	3ad2ant1	|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
3		ceqsalt	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
4	3	3comr	|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A. x ( x = A -> ph ) <-> ps ) )
5	2 4	bitrd	|- ( ( A e. V /\ F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( [. A / x ]. ph <-> ps ) )