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

Metamath Proof Explorer

Theorem riotasbc

Description: Substitution law for descriptions. Compare iotasbc . (Contributed by NM, 23-Aug-2011) (Proof shortened by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Assertion	riotasbc	$⊢ \exists! x \in A φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ$

Proof

Step	Hyp	Ref	Expression
1		rabssab	$⊢ \{x \in A \| φ\} \subseteq \{x \| φ\}$
2		riotacl2	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) \in \{x \in A \| φ\}$
3	1 2	sselid	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) \in \{x \| φ\}$
4		df-sbc	$⊢ \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ \leftrightarrow (ι x \in A \| φ) \in \{x \| φ\}$
5	3 4	sylibr	$⊢ \exists! x \in A φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ$