Theorem eqsbc1

Description: Substitution for the left-hand side in an equality. Class version of eqsb1 . (Contributed by Andrew Salmon, 29-Jun-2011) Avoid ax-13 . (Revised by Wolf Lammen, 29-Apr-2023)

	Ref	Expression
Assertion	eqsbc1	|- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	|- ( y = A -> ( [. y / x ]. x = B <-> [. A / x ]. x = B ) )
2		eqeq1	|- ( y = A -> ( y = B <-> A = B ) )
3		sbsbc	|- ( [ y / x ] x = B <-> [. y / x ]. x = B )
4		eqsb1	|- ( [ y / x ] x = B <-> y = B )
5	3 4	bitr3i	|- ( [. y / x ]. x = B <-> y = B )
6	1 2 5	vtoclbg	|- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )