Theorem sbceqi

Description: Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypotheses	sbceqi.1	⊢ 𝐴 ∈ V
	sbceqi.2	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷
	sbceqi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐸
Assertion	sbceqi	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ 𝐷 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		sbceqi.1	⊢ 𝐴 ∈ V
2		sbceqi.2	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷
3		sbceqi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐸
4		sbceqg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
5	1 4	ax-mp	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
6	2 3	eqeq12i	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝐷 = 𝐸 )
7	5 6	bitri	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ 𝐷 = 𝐸 )