Metamath Proof Explorer

Theorem rmo4

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypothesis rmo4.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion rmo4 
|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 rmo4.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
3 an4 
 |-  ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) )
4 ancom 
 |-  ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
5 4 anbi1i 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
6 3 5 bitri 
 |-  ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
7 6 imbi1i 
 |-  ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) )
8 impexp 
 |-  ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ ps ) -> x = y ) ) )
9 impexp 
 |-  ( ( ( y e. A /\ x e. A ) -> ( ( ph /\ ps ) -> x = y ) ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
10 7 8 9 3bitri 
 |-  ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
11 10 albii 
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
12 df-ral 
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
13 r19.21v 
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) <-> ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
14 11 12 13 3bitr2i 
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
15 14 albii 
 |-  ( A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
16 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
17 16 1 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
18 17 mo4 
 |-  ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) )
19 df-ral 
 |-  ( A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
20 15 18 19 3bitr4i 
 |-  ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
21 2 20 bitri 
 |-  ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )