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

Metamath Proof Explorer

Theorem sbcie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004)

	Ref	Expression
Hypotheses	sbcie.1	$⊢ A \in V$
	sbcie.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	sbcie	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow ψ$

Step	Hyp	Ref	Expression
1		sbcie.1	$⊢ A \in V$
2		sbcie.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
3	2	sbcieg	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow ψ)$
4	1 3	ax-mp	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow ψ$