This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( { 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 ) )