Metamath Proof Explorer

Theorem rmo3

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) Avoid ax-13 . (Revised by Wolf Lammen, 30-Apr-2023)

Ref Expression
Hypothesis rmo2.1 
|- F/ y ph
Assertion rmo3 
|- ( 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 rmo2.1 
 |-  F/ y ph
2 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
3 sban 
 |-  ( [ y / x ] ( x e. A /\ ph ) <-> ( [ y / x ] x e. A /\ [ y / x ] ph ) )
4 clelsb1 
 |-  ( [ y / x ] x e. A <-> y e. A )
5 4 anbi1i 
 |-  ( ( [ y / x ] x e. A /\ [ y / x ] ph ) <-> ( y e. A /\ [ y / x ] ph ) )
6 3 5 bitri 
 |-  ( [ y / x ] ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) )
7 6 anbi2i 
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) )
8 an4 
 |-  ( ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
9 ancom 
 |-  ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
10 9 anbi1i 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
11 7 8 10 3bitri 
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
12 11 imbi1i 
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) )
13 impexp 
 |-  ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
14 impexp 
 |-  ( ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
15 12 13 14 3bitri 
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
16 15 albii 
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
17 df-ral 
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
18 r19.21v 
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
19 16 17 18 3bitr2i 
 |-  ( 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 ) ) )
20 19 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 ) ) )
21 nfv 
 |-  F/ y x e. A
22 21 1 nfan 
 |-  F/ y ( x e. A /\ ph )
23 22 mo3 
 |-  ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) )
24 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 ) ) )
25 20 23 24 3bitr4i 
 |-  ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
26 2 25 bitri 
 |-  ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )