Metamath Proof Explorer

Theorem riotasv3d

Description: A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 ) also holds for its description binder D (in the form of property th ). (Contributed by NM, 5-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 riotasv3d.1 
 |-  F/ y ph
2 riotasv3d.2 
 |-  ( ph -> F/ y th )
3 riotasv3d.3 
 |-  ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
4 riotasv3d.4 
 |-  ( ( ph /\ C = D ) -> ( ch <-> th ) )
5 riotasv3d.5 
 |-  ( ph -> ( ( y e. B /\ ps ) -> ch ) )
6 riotasv3d.6 
 |-  ( ph -> D e. A )
7 riotasv3d.7 
 |-  ( ph -> E. y e. B ps )
8 elex 
 |-  ( A e. V -> A e. _V )
9 7 adantr 
 |-  ( ( ph /\ A e. _V ) -> E. y e. B ps )
10 nfv 
 |-  F/ y A e. _V
11 5 imp 
 |-  ( ( ph /\ ( y e. B /\ ps ) ) -> ch )
12 11 adantrl 
 |-  ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> ch )
13 3 6 riotasvd 
 |-  ( ( ph /\ A e. _V ) -> ( ( y e. B /\ ps ) -> D = C ) )
14 13 impr 
 |-  ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> D = C )
15 14 eqcomd 
 |-  ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> C = D )
16 15 4 syldan 
 |-  ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> ( ch <-> th ) )
17 12 16 mpbid 
 |-  ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> th )
18 17 exp45 
 |-  ( ph -> ( A e. _V -> ( y e. B -> ( ps -> th ) ) ) )
19 1 10 18 ralrimd 
 |-  ( ph -> ( A e. _V -> A. y e. B ( ps -> th ) ) )
20 r19.23t 
 |-  ( F/ y th -> ( A. y e. B ( ps -> th ) <-> ( E. y e. B ps -> th ) ) )
21 2 20 syl 
 |-  ( ph -> ( A. y e. B ( ps -> th ) <-> ( E. y e. B ps -> th ) ) )
22 19 21 sylibd 
 |-  ( ph -> ( A e. _V -> ( E. y e. B ps -> th ) ) )
23 22 imp 
 |-  ( ( ph /\ A e. _V ) -> ( E. y e. B ps -> th ) )
24 9 23 mpd 
 |-  ( ( ph /\ A e. _V ) -> th )
25 8 24 sylan2 
 |-  ( ( ph /\ A e. V ) -> th )