Metamath Proof Explorer

Theorem riotasv

Description: Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ). Special case of riota2f . (Contributed by NM, 26-Jan-2013) (Proof shortened by Mario Carneiro, 6-Dec-2016)

	Ref	Expression
Hypotheses	riotasv.1	$⊢ A \in V$
	riotasv.2	$⊢ D = (ι x \in A \| \forall y \in B (φ \to x = C))$
Assertion	riotasv	$⊢ (D \in A \land y \in B \land φ) \to D = C$

Proof

Step	Hyp	Ref	Expression
1		riotasv.1	$⊢ A \in V$
2		riotasv.2	$⊢ D = (ι x \in A \| \forall y \in B (φ \to x = C))$
3	2	a1i	$⊢ D \in A \to D = (ι x \in A \| \forall y \in B (φ \to x = C))$
4		id	$⊢ D \in A \to D \in A$
5	3 4	riotasvd	$⊢ (D \in A \land A \in V) \to ((y \in B \land φ) \to D = C)$
6	1 5	mpan2	$⊢ D \in A \to ((y \in B \land φ) \to D = C)$
7	6	3impib	$⊢ (D \in A \land y \in B \land φ) \to D = C$