Metamath Proof Explorer


Theorem eusvobj2

Description: Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis eusvobj1.1
|- B e. _V
Assertion eusvobj2
|- ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) )

Proof

Step Hyp Ref Expression
1 eusvobj1.1
 |-  B e. _V
2 euabsn2
 |-  ( E! x E. y e. A x = B <-> E. z { x | E. y e. A x = B } = { z } )
3 eleq2
 |-  ( { x | E. y e. A x = B } = { z } -> ( x e. { x | E. y e. A x = B } <-> x e. { z } ) )
4 abid
 |-  ( x e. { x | E. y e. A x = B } <-> E. y e. A x = B )
5 velsn
 |-  ( x e. { z } <-> x = z )
6 3 4 5 3bitr3g
 |-  ( { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B <-> x = z ) )
7 nfre1
 |-  F/ y E. y e. A x = B
8 7 nfab
 |-  F/_ y { x | E. y e. A x = B }
9 8 nfeq1
 |-  F/ y { x | E. y e. A x = B } = { z }
10 1 elabrex
 |-  ( y e. A -> B e. { x | E. y e. A x = B } )
11 eleq2
 |-  ( { x | E. y e. A x = B } = { z } -> ( B e. { x | E. y e. A x = B } <-> B e. { z } ) )
12 1 elsn
 |-  ( B e. { z } <-> B = z )
13 eqcom
 |-  ( B = z <-> z = B )
14 12 13 bitri
 |-  ( B e. { z } <-> z = B )
15 11 14 bitrdi
 |-  ( { x | E. y e. A x = B } = { z } -> ( B e. { x | E. y e. A x = B } <-> z = B ) )
16 10 15 syl5ib
 |-  ( { x | E. y e. A x = B } = { z } -> ( y e. A -> z = B ) )
17 9 16 ralrimi
 |-  ( { x | E. y e. A x = B } = { z } -> A. y e. A z = B )
18 eqeq1
 |-  ( x = z -> ( x = B <-> z = B ) )
19 18 ralbidv
 |-  ( x = z -> ( A. y e. A x = B <-> A. y e. A z = B ) )
20 17 19 syl5ibrcom
 |-  ( { x | E. y e. A x = B } = { z } -> ( x = z -> A. y e. A x = B ) )
21 6 20 sylbid
 |-  ( { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B -> A. y e. A x = B ) )
22 21 exlimiv
 |-  ( E. z { x | E. y e. A x = B } = { z } -> ( E. y e. A x = B -> A. y e. A x = B ) )
23 2 22 sylbi
 |-  ( E! x E. y e. A x = B -> ( E. y e. A x = B -> A. y e. A x = B ) )
24 euex
 |-  ( E! x E. y e. A x = B -> E. x E. y e. A x = B )
25 rexn0
 |-  ( E. y e. A x = B -> A =/= (/) )
26 25 exlimiv
 |-  ( E. x E. y e. A x = B -> A =/= (/) )
27 r19.2z
 |-  ( ( A =/= (/) /\ A. y e. A x = B ) -> E. y e. A x = B )
28 27 ex
 |-  ( A =/= (/) -> ( A. y e. A x = B -> E. y e. A x = B ) )
29 24 26 28 3syl
 |-  ( E! x E. y e. A x = B -> ( A. y e. A x = B -> E. y e. A x = B ) )
30 23 29 impbid
 |-  ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) )