Metamath Proof Explorer

Theorem reu6

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

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

Proof

Step Hyp Ref Expression
1 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2 19.28v 
 |-  ( A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) <-> ( y e. A /\ A. x ( x e. A -> ( ph <-> x = y ) ) ) )
3 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
4 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
5 3 4 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) ) )
6 equequ1 
 |-  ( x = y -> ( x = y <-> y = y ) )
7 5 6 bibi12d 
 |-  ( x = y -> ( ( ( x e. A /\ ph ) <-> x = y ) <-> ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) ) )
8 equid 
 |-  y = y
9 8 tbt 
 |-  ( ( y e. A /\ [ y / x ] ph ) <-> ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) )
10 simpl 
 |-  ( ( y e. A /\ [ y / x ] ph ) -> y e. A )
11 9 10 sylbir 
 |-  ( ( ( y e. A /\ [ y / x ] ph ) <-> y = y ) -> y e. A )
12 7 11 syl6bi 
 |-  ( x = y -> ( ( ( x e. A /\ ph ) <-> x = y ) -> y e. A ) )
13 12 spimvw 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> y e. A )
14 ibar 
 |-  ( x e. A -> ( ph <-> ( x e. A /\ ph ) ) )
15 14 bibi1d 
 |-  ( x e. A -> ( ( ph <-> x = y ) <-> ( ( x e. A /\ ph ) <-> x = y ) ) )
16 15 biimprcd 
 |-  ( ( ( x e. A /\ ph ) <-> x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
17 16 sps 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
18 13 17 jca 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
19 18 axc4i 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) -> A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
20 biimp 
 |-  ( ( ph <-> x = y ) -> ( ph -> x = y ) )
21 20 imim2i 
 |-  ( ( x e. A -> ( ph <-> x = y ) ) -> ( x e. A -> ( ph -> x = y ) ) )
22 21 impd 
 |-  ( ( x e. A -> ( ph <-> x = y ) ) -> ( ( x e. A /\ ph ) -> x = y ) )
23 22 adantl 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( ( x e. A /\ ph ) -> x = y ) )
24 3 biimprcd 
 |-  ( y e. A -> ( x = y -> x e. A ) )
25 24 adantr 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( x = y -> x e. A ) )
26 25 imp 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> x e. A )
27 simplr 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A -> ( ph <-> x = y ) ) )
28 simpr 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> x = y )
29 biimpr 
 |-  ( ( ph <-> x = y ) -> ( x = y -> ph ) )
30 27 28 29 syl6ci 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A -> ph ) )
31 26 30 jcai 
 |-  ( ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) /\ x = y ) -> ( x e. A /\ ph ) )
32 31 ex 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( x = y -> ( x e. A /\ ph ) ) )
33 23 32 impbid 
 |-  ( ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> ( ( x e. A /\ ph ) <-> x = y ) )
34 33 alimi 
 |-  ( A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) -> A. x ( ( x e. A /\ ph ) <-> x = y ) )
35 19 34 impbii 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) <-> A. x ( y e. A /\ ( x e. A -> ( ph <-> x = y ) ) ) )
36 df-ral 
 |-  ( A. x e. A ( ph <-> x = y ) <-> A. x ( x e. A -> ( ph <-> x = y ) ) )
37 36 anbi2i 
 |-  ( ( y e. A /\ A. x e. A ( ph <-> x = y ) ) <-> ( y e. A /\ A. x ( x e. A -> ( ph <-> x = y ) ) ) )
38 2 35 37 3bitr4i 
 |-  ( A. x ( ( x e. A /\ ph ) <-> x = y ) <-> ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
39 38 exbii 
 |-  ( E. y A. x ( ( x e. A /\ ph ) <-> x = y ) <-> E. y ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
40 eu6 
 |-  ( E! x ( x e. A /\ ph ) <-> E. y A. x ( ( x e. A /\ ph ) <-> x = y ) )
41 df-rex 
 |-  ( E. y e. A A. x e. A ( ph <-> x = y ) <-> E. y ( y e. A /\ A. x e. A ( ph <-> x = y ) ) )
42 39 40 41 3bitr4i 
 |-  ( E! x ( x e. A /\ ph ) <-> E. y e. A A. x e. A ( ph <-> x = y ) )
43 1 42 bitri 
 |-  ( E! x e. A ph <-> E. y e. A A. x e. A ( ph <-> x = y ) )