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 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 )