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\in \mathrm{V}$$
	sbceqi.2	$$⊢⦋A/x⦌B=D$$
	sbceqi.3	$$⊢⦋A/x⦌C=E$$
Assertion	sbceqi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow D=E$$

Proof

Step	Hyp	Ref	Expression
1		sbceqi.1	$$⊢A\in \mathrm{V}$$
2		sbceqi.2	$$⊢⦋A/x⦌B=D$$
3		sbceqi.3	$$⊢⦋A/x⦌C=E$$
4		sbceqg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow ⦋A/x⦌B=⦋A/x⦌C\right)$$
5	1 4	ax-mp	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow ⦋A/x⦌B=⦋A/x⦌C$$
6	2 3	eqeq12i	$$⊢⦋A/x⦌B=⦋A/x⦌C\leftrightarrow D=E$$
7	5 6	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow D=E$$