Theorem sbceqi

Description: Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypotheses	sbceqi.1	|- A e. _V
	sbceqi.2	|- [_ A / x ]_ B = D
	sbceqi.3	|- [_ A / x ]_ C = E
Assertion	sbceqi	|- ( [. A / x ]. B = C <-> D = E )

Proof

Step	Hyp	Ref	Expression
1		sbceqi.1	|- A e. _V
2		sbceqi.2	|- [_ A / x ]_ B = D
3		sbceqi.3	|- [_ A / x ]_ C = E
4		sbceqg	|- ( A e. _V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
5	1 4	ax-mp	|- ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C )
6	2 3	eqeq12i	|- ( [_ A / x ]_ B = [_ A / x ]_ C <-> D = E )
7	5 6	bitri	|- ( [. A / x ]. B = C <-> D = E )