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

Metamath Proof Explorer

Theorem csbeq2i

Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis csbeq2i.1 ⊢ 𝐵 = 𝐶
Assertion csbeq2i ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶

Proof

Step Hyp Ref Expression
1 csbeq2i.1 ⊢ 𝐵 = 𝐶
2 1 a1i ⊢ ( ⊤ → 𝐵 = 𝐶 )
3 2 csbeq2dv ⊢ ( ⊤ → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
4 3 mptru ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶