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