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

Metamath Proof Explorer

Theorem sbcbii

Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005)

		Ref	Expression
	Hypothesis	sbcbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	sbcbii	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} ψ$

Step	Hyp	Ref	Expression
1		sbcbii.1	$⊢ φ \leftrightarrow ψ$
2	1	a1i	$⊢ ⊤ \to (φ \leftrightarrow ψ)$
3	2	sbcbidv	$⊢ ⊤ \to (\underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} ψ)$
4	3	mptru	$⊢ \underset{˙}{[} A / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} ψ$