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

Metamath Proof Explorer

Theorem sbc6

Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Proof shortened by Eric Schmidt, 17-Jan-2007)

		Ref	Expression
	Hypothesis	sbc6.1	$⊢ A \in V$
	Assertion	sbc6	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow \forall x (x = A \to φ)$

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