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	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) )
2		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝐴 = 𝐵 ) )
3		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑥 = 𝐵 )
4		eqsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐵 ↔ 𝑦 = 𝐵 )
5	3 4	bitr3i	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐵 ↔ 𝑦 = 𝐵 )
6	1 2 5	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )