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 )