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

Metamath Proof Explorer

Theorem iotasbcq

Description: Theorem *14.272 in WhiteheadRussell p. 193. (Contributed by Andrew Salmon, 11-Jul-2011)

		Ref	Expression
	Assertion	iotasbcq	$⊢ \forall x (φ \leftrightarrow ψ) \to (\underset{˙}{[} (ι x \| φ) / y \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} (ι x \| ψ) / y \underset{˙}{]} χ)$

Step	Hyp	Ref	Expression
1		iotabi	$⊢ \forall x (φ \leftrightarrow ψ) \to (ι x \| φ) = (ι x \| ψ)$
2	1	sbceq1d	$⊢ \forall x (φ \leftrightarrow ψ) \to (\underset{˙}{[} (ι x \| φ) / y \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} (ι x \| ψ) / y \underset{˙}{]} χ)$