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 )