Theorem eqsbc2

Description: Substitution for the right-hand side in an equality. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 7-Jul-2021)

	Ref	Expression
Assertion	eqsbc2	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=x\leftrightarrow B=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqsbc1	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=B\leftrightarrow A=B\right)$$
2		eqcom	$$⊢B=x\leftrightarrow x=B$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=x\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=B$$
4		eqcom	$$⊢B=A\leftrightarrow A=B$$
5	1 3 4	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=x\leftrightarrow B=A\right)$$