Theorem csbied

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

	Ref	Expression
Hypotheses	csbied.1	|- ( ph -> A e. V )
	csbied.2	|- ( ( ph /\ x = A ) -> B = C )
Assertion	csbied	|- ( ph -> [_ A / x ]_ B = C )

Proof

Step	Hyp	Ref	Expression
1		csbied.1	|- ( ph -> A e. V )
2		csbied.2	|- ( ( ph /\ x = A ) -> B = C )
3		df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
4	2	eleq2d	|- ( ( ph /\ x = A ) -> ( z e. B <-> z e. C ) )
5	1 4	sbcied	|- ( ph -> ( [. A / x ]. z e. B <-> z e. C ) )
6	5	alrimiv	|- ( ph -> A. z ( [. A / x ]. z e. B <-> z e. C ) )
7		df-clab	|- ( z e. { y | [. A / x ]. y e. B } <-> [ z / y ] [. A / x ]. y e. B )
8		eleq1w	|- ( y = z -> ( y e. B <-> z e. B ) )
9	8	sbcbidv	|- ( y = z -> ( [. A / x ]. y e. B <-> [. A / x ]. z e. B ) )
10	9	sbievw	|- ( [ z / y ] [. A / x ]. y e. B <-> [. A / x ]. z e. B )
11	7 10	bitr2i	|- ( [. A / x ]. z e. B <-> z e. { y | [. A / x ]. y e. B } )
12	11	bibi1i	|- ( ( [. A / x ]. z e. B <-> z e. C ) <-> ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
13	12	biimpi	|- ( ( [. A / x ]. z e. B <-> z e. C ) -> ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
14	6 13	sylg	|- ( ph -> A. z ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
15		dfcleq	|- ( { y | [. A / x ]. y e. B } = C <-> A. z ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
16	14 15	sylibr	|- ( ph -> { y | [. A / x ]. y e. B } = C )
17	3 16	eqtrid	|- ( ph -> [_ A / x ]_ B = C )