Theorem csbie

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024)

	Ref	Expression
Hypotheses	csbie.1	|- A e. _V
	csbie.2	|- ( x = A -> B = C )
Assertion	csbie	|- [_ A / x ]_ B = C

Proof

Step	Hyp	Ref	Expression
1		csbie.1	|- A e. _V
2		csbie.2	|- ( x = A -> B = C )
3		df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
4	2	eleq2d	|- ( x = A -> ( y e. B <-> y e. C ) )
5	1 4	sbcie	|- ( [. A / x ]. y e. B <-> y e. C )
6	5	abbii	|- { y | [. A / x ]. y e. B } = { y | y e. C }
7		abid2	|- { y | y e. C } = C
8	3 6 7	3eqtri	|- [_ A / x ]_ B = C