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

Metamath Proof Explorer

Theorem csbiegf

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypotheses	csbiegf.1	$⊢ A \in V \to \underline{Ⅎ} x C$
	csbiegf.2	$⊢ x = A \to B = C$
Assertion	csbiegf	$⊢ A \in V \to ⦋ A / x ⦌ B = C$

Proof

Step	Hyp	Ref	Expression
1		csbiegf.1	$⊢ A \in V \to \underline{Ⅎ} x C$
2		csbiegf.2	$⊢ x = A \to B = C$
3	2	ax-gen	$⊢ \forall x (x = A \to B = C)$
4		csbiebt	$⊢ (A \in V \land \underline{Ⅎ} x C) \to (\forall x (x = A \to B = C) \leftrightarrow ⦋ A / x ⦌ B = C)$
5	1 4	mpdan	$⊢ A \in V \to (\forall x (x = A \to B = C) \leftrightarrow ⦋ A / x ⦌ B = C)$
6	3 5	mpbii	$⊢ A \in V \to ⦋ A / x ⦌ B = C$