This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbceqi

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

Ref Expression
Hypotheses sbceqi.1 ⊢ A ∈ V
sbceqi.2 ⊢ ⦋ A / x⦌ B = D
sbceqi.3 ⊢ ⦋ A / x⦌ C = E
Assertion sbceqi ⊢ [˙A / x]˙ B = C ↔ D = E

Proof

Step Hyp Ref Expression
1 sbceqi.1 ⊢ A ∈ V
2 sbceqi.2 ⊢ ⦋ A / x⦌ B = D
3 sbceqi.3 ⊢ ⦋ A / x⦌ C = E
4 sbceqg ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C
5 1 4 ax-mp ⊢ [˙A / x]˙ B = C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C
6 2 3 eqeq12i ⊢ ⦋ A / x⦌ B = ⦋ A / x⦌ C ↔ D = E
7 5 6 bitri ⊢ [˙A / x]˙ B = C ↔ D = E