Metamath Proof Explorer

Theorem reu3

Description: A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006)

Ref Expression
Assertion reu3 
|- ( E! x e. A ph <-> ( E. x e. A ph /\ E. y e. A A. x e. A ( ph -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 reurex 
 |-  ( E! x e. A ph -> E. x e. A ph )
2 reu6 
 |-  ( E! x e. A ph <-> E. y e. A A. x e. A ( ph <-> x = y ) )
3 biimp 
 |-  ( ( ph <-> x = y ) -> ( ph -> x = y ) )
4 3 ralimi 
 |-  ( A. x e. A ( ph <-> x = y ) -> A. x e. A ( ph -> x = y ) )
5 4 reximi 
 |-  ( E. y e. A A. x e. A ( ph <-> x = y ) -> E. y e. A A. x e. A ( ph -> x = y ) )
6 2 5 sylbi 
 |-  ( E! x e. A ph -> E. y e. A A. x e. A ( ph -> x = y ) )
7 1 6 jca 
 |-  ( E! x e. A ph -> ( E. x e. A ph /\ E. y e. A A. x e. A ( ph -> x = y ) ) )
8 rexex 
 |-  ( E. y e. A A. x e. A ( ph -> x = y ) -> E. y A. x e. A ( ph -> x = y ) )
9 8 anim2i 
 |-  ( ( E. x e. A ph /\ E. y e. A A. x e. A ( ph -> x = y ) ) -> ( E. x e. A ph /\ E. y A. x e. A ( ph -> x = y ) ) )
10 eu3v 
 |-  ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ E. y A. x ( ( x e. A /\ ph ) -> x = y ) ) )
11 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
12 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
13 df-ral 
 |-  ( A. x e. A ( ph -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
14 impexp 
 |-  ( ( ( x e. A /\ ph ) -> x = y ) <-> ( x e. A -> ( ph -> x = y ) ) )
15 14 albii 
 |-  ( A. x ( ( x e. A /\ ph ) -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
16 13 15 bitr4i 
 |-  ( A. x e. A ( ph -> x = y ) <-> A. x ( ( x e. A /\ ph ) -> x = y ) )
17 16 exbii 
 |-  ( E. y A. x e. A ( ph -> x = y ) <-> E. y A. x ( ( x e. A /\ ph ) -> x = y ) )
18 12 17 anbi12i 
 |-  ( ( E. x e. A ph /\ E. y A. x e. A ( ph -> x = y ) ) <-> ( E. x ( x e. A /\ ph ) /\ E. y A. x ( ( x e. A /\ ph ) -> x = y ) ) )
19 10 11 18 3bitr4i 
 |-  ( E! x e. A ph <-> ( E. x e. A ph /\ E. y A. x e. A ( ph -> x = y ) ) )
20 9 19 sylibr 
 |-  ( ( E. x e. A ph /\ E. y e. A A. x e. A ( ph -> x = y ) ) -> E! x e. A ph )
21 7 20 impbii 
 |-  ( E! x e. A ph <-> ( E. x e. A ph /\ E. y e. A A. x e. A ( ph -> x = y ) ) )