Metamath Proof Explorer


Theorem riotasv2d

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, 2-Mar-2013)

Ref Expression
Hypotheses riotasv2d.1
|- F/ y ph
riotasv2d.2
|- ( ph -> F/_ y F )
riotasv2d.3
|- ( ph -> F/ y ch )
riotasv2d.4
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
riotasv2d.5
|- ( ( ph /\ y = E ) -> ( ps <-> ch ) )
riotasv2d.6
|- ( ( ph /\ y = E ) -> C = F )
riotasv2d.7
|- ( ph -> D e. A )
riotasv2d.8
|- ( ph -> E e. B )
riotasv2d.9
|- ( ph -> ch )
Assertion riotasv2d
|- ( ( ph /\ A e. V ) -> D = F )

Proof

Step Hyp Ref Expression
1 riotasv2d.1
 |-  F/ y ph
2 riotasv2d.2
 |-  ( ph -> F/_ y F )
3 riotasv2d.3
 |-  ( ph -> F/ y ch )
4 riotasv2d.4
 |-  ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
5 riotasv2d.5
 |-  ( ( ph /\ y = E ) -> ( ps <-> ch ) )
6 riotasv2d.6
 |-  ( ( ph /\ y = E ) -> C = F )
7 riotasv2d.7
 |-  ( ph -> D e. A )
8 riotasv2d.8
 |-  ( ph -> E e. B )
9 riotasv2d.9
 |-  ( ph -> ch )
10 elex
 |-  ( A e. V -> A e. _V )
11 8 adantr
 |-  ( ( ph /\ A e. _V ) -> E e. B )
12 9 adantr
 |-  ( ( ph /\ A e. _V ) -> ch )
13 eleq1
 |-  ( y = E -> ( y e. B <-> E e. B ) )
14 13 adantl
 |-  ( ( ph /\ y = E ) -> ( y e. B <-> E e. B ) )
15 14 5 anbi12d
 |-  ( ( ph /\ y = E ) -> ( ( y e. B /\ ps ) <-> ( E e. B /\ ch ) ) )
16 6 eqeq2d
 |-  ( ( ph /\ y = E ) -> ( D = C <-> D = F ) )
17 15 16 imbi12d
 |-  ( ( ph /\ y = E ) -> ( ( ( y e. B /\ ps ) -> D = C ) <-> ( ( E e. B /\ ch ) -> D = F ) ) )
18 17 adantlr
 |-  ( ( ( ph /\ A e. _V ) /\ y = E ) -> ( ( ( y e. B /\ ps ) -> D = C ) <-> ( ( E e. B /\ ch ) -> D = F ) ) )
19 4 7 riotasvd
 |-  ( ( ph /\ A e. _V ) -> ( ( y e. B /\ ps ) -> D = C ) )
20 nfv
 |-  F/ y A e. _V
21 1 20 nfan
 |-  F/ y ( ph /\ A e. _V )
22 nfcvd
 |-  ( ( ph /\ A e. _V ) -> F/_ y E )
23 nfvd
 |-  ( ph -> F/ y E e. B )
24 23 3 nfand
 |-  ( ph -> F/ y ( E e. B /\ ch ) )
25 nfra1
 |-  F/ y A. y e. B ( ps -> x = C )
26 nfcv
 |-  F/_ y A
27 25 26 nfriota
 |-  F/_ y ( iota_ x e. A A. y e. B ( ps -> x = C ) )
28 1 4 nfceqdf
 |-  ( ph -> ( F/_ y D <-> F/_ y ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) )
29 27 28 mpbiri
 |-  ( ph -> F/_ y D )
30 29 2 nfeqd
 |-  ( ph -> F/ y D = F )
31 24 30 nfimd
 |-  ( ph -> F/ y ( ( E e. B /\ ch ) -> D = F ) )
32 31 adantr
 |-  ( ( ph /\ A e. _V ) -> F/ y ( ( E e. B /\ ch ) -> D = F ) )
33 11 18 19 21 22 32 vtocldf
 |-  ( ( ph /\ A e. _V ) -> ( ( E e. B /\ ch ) -> D = F ) )
34 11 12 33 mp2and
 |-  ( ( ph /\ A e. _V ) -> D = F )
35 10 34 sylan2
 |-  ( ( ph /\ A e. V ) -> D = F )