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 e. _V
	riotasv.2	|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )
Assertion	riotasv	|- ( ( D e. A /\ y e. B /\ ph ) -> D = C )

Proof

Step	Hyp	Ref	Expression
1		riotasv.1	|- A e. _V
2		riotasv.2	|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )
3	2	a1i	|- ( D e. A -> D = ( iota_ x e. A A. y e. B ( ph -> x = C ) ) )
4		id	|- ( D e. A -> D e. A )
5	3 4	riotasvd	|- ( ( D e. A /\ A e. _V ) -> ( ( y e. B /\ ph ) -> D = C ) )
6	1 5	mpan2	|- ( D e. A -> ( ( y e. B /\ ph ) -> D = C ) )
7	6	3impib	|- ( ( D e. A /\ y e. B /\ ph ) -> D = C )