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

Metamath Proof Explorer

Theorem reu2

Description: A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994)

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

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ( x e. A /\ ph )
2 1 eu2 
 |-  ( E! x ( x e. A /\ ph ) <-> ( E. x ( x e. A /\ ph ) /\ A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) ) )
3 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
4 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5 df-ral 
 |-  ( A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
6 19.21v 
 |-  ( A. y ( x e. A -> ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) <-> ( x e. A -> A. y ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
7 nfv 
 |-  F/ x y e. A
8 nfs1v 
 |-  F/ x [ y / x ] ph
9 7 8 nfan 
 |-  F/ x ( y e. A /\ [ y / x ] ph )
10 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
11 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
12 10 11 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) ) )
13 9 12 sbiev 
 |-  ( [ y / x ] ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) )
14 13 anbi2i 
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) )
15 an4 
 |-  ( ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
16 14 15 bitri 
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
17 16 imbi1i 
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) )
18 impexp 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
19 impexp 
 |-  ( ( ( x e. A /\ y e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( x e. A -> ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
20 17 18 19 3bitri 
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( x e. A -> ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
21 20 albii 
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. y ( x e. A -> ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
22 df-ral 
 |-  ( A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. y ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
23 22 imbi2i 
 |-  ( ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( x e. A -> A. y ( y e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
24 6 21 23 3bitr4i 
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
25 24 albii 
 |-  ( A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
26 5 25 bitr4i 
 |-  ( A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) )
27 4 26 anbi12i 
 |-  ( ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( E. x ( x e. A /\ ph ) /\ A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) ) )
28 2 3 27 3bitr4i 
 |-  ( E! x e. A ph <-> ( E. x e. A ph /\ A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )