Theorem sbceqbidf

Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018)

	Ref	Expression
Hypotheses	sbceqbidf.1	$$⊢Ⅎx\phi$$
	sbceqbidf.2	$$⊢\phi \to A=B$$
	sbceqbidf.3	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbceqbidf	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbceqbidf.1	$$⊢Ⅎx\phi$$
2		sbceqbidf.2	$$⊢\phi \to A=B$$
3		sbceqbidf.3	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
4	1 3	abbid	$$⊢\phi \to \left\{x|\psi \right\}=\left\{x|\chi \right\}$$
5	2 4	eleq12d	$$⊢\phi \to \left(A\in \left\{x|\psi \right\}\leftrightarrow B\in \left\{x|\chi \right\}\right)$$
6		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow A\in \left\{x|\psi \right\}$$
7		df-sbc	$$⊢\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi \leftrightarrow B\in \left\{x|\chi \right\}$$
8	5 6 7	3bitr4g	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi \right)$$