Theorem eqsbc3

Description: Substitution applied to an atomic wff. Class version of eqsb3 . (Contributed by Andrew Salmon, 29-Jun-2011) Avoid ax-13 . (Revised by Wolf Lammen, 29-Apr-2023)

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

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=B\right)$$
2		eqeq1	$$⊢y=A\to \left(y=B\leftrightarrow A=B\right)$$
3		sbsbc	$$⊢\left[y/x\right]x=B\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=B$$
4		eqsb3	$$⊢\left[y/x\right]x=B\leftrightarrow y=B$$
5	3 4	bitr3i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=B\leftrightarrow y=B$$
6	1 2 5	vtoclbg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=B\leftrightarrow A=B\right)$$