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

Metamath Proof Explorer

Theorem csbeq12dv

Description: Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023)

Ref Expression
Hypotheses csbeq12dv.1 ⊢ φ → A = C
csbeq12dv.2 ⊢ φ → B = D
Assertion csbeq12dv ⊢ φ → ⦋ A / x⦌ B = ⦋ C / x⦌ D

Proof

Step Hyp Ref Expression
1 csbeq12dv.1 ⊢ φ → A = C
2 csbeq12dv.2 ⊢ φ → B = D
3 1 csbeq1d ⊢ φ → ⦋ A / x⦌ B = ⦋ C / x⦌ B
4 2 csbeq2dv ⊢ φ → ⦋ C / x⦌ B = ⦋ C / x⦌ D
5 3 4 eqtrd ⊢ φ → ⦋ A / x⦌ B = ⦋ C / x⦌ D