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	$⊢ B = C$
	Assertion	csbeq2i	$⊢ ⦋ A / x ⦌ B = ⦋ A / x ⦌ C$

Step	Hyp	Ref	Expression
1		csbeq2i.1	$⊢ B = C$
2	1	a1i	$⊢ ⊤ \to B = C$
3	2	csbeq2dv	$⊢ ⊤ \to ⦋ A / x ⦌ B = ⦋ A / x ⦌ C$
4	3	mptru	$⊢ ⦋ A / x ⦌ B = ⦋ A / x ⦌ C$