Metamath Proof Explorer

Theorem mo5f

Description: Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017)

Ref Expression
Hypotheses mo5f.1 
|- F/ i ph
mo5f.2 
|- F/ j ph
Assertion mo5f 
|- ( E* x ph <-> A. i A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )

Proof

Step Hyp Ref Expression
1 mo5f.1 
 |-  F/ i ph
2 mo5f.2 
 |-  F/ j ph
3 2 mo3 
 |-  ( E* x ph <-> A. x A. j ( ( ph /\ [ j / x ] ph ) -> x = j ) )
4 1 nfsbv 
 |-  F/ i [ j / x ] ph
5 1 4 nfan 
 |-  F/ i ( ph /\ [ j / x ] ph )
6 nfv 
 |-  F/ i x = j
7 5 6 nfim 
 |-  F/ i ( ( ph /\ [ j / x ] ph ) -> x = j )
8 7 nfal 
 |-  F/ i A. j ( ( ph /\ [ j / x ] ph ) -> x = j )
9 8 sb8f 
 |-  ( A. x A. j ( ( ph /\ [ j / x ] ph ) -> x = j ) <-> A. i [ i / x ] A. j ( ( ph /\ [ j / x ] ph ) -> x = j ) )
10 sbim 
 |-  ( [ i / x ] ( ( ph /\ [ j / x ] ph ) -> x = j ) <-> ( [ i / x ] ( ph /\ [ j / x ] ph ) -> [ i / x ] x = j ) )
11 sban 
 |-  ( [ i / x ] ( ph /\ [ j / x ] ph ) <-> ( [ i / x ] ph /\ [ i / x ] [ j / x ] ph ) )
12 nfs1v 
 |-  F/ x [ j / x ] ph
13 12 sbf 
 |-  ( [ i / x ] [ j / x ] ph <-> [ j / x ] ph )
14 13 bicomi 
 |-  ( [ j / x ] ph <-> [ i / x ] [ j / x ] ph )
15 14 anbi2i 
 |-  ( ( [ i / x ] ph /\ [ j / x ] ph ) <-> ( [ i / x ] ph /\ [ i / x ] [ j / x ] ph ) )
16 11 15 bitr4i 
 |-  ( [ i / x ] ( ph /\ [ j / x ] ph ) <-> ( [ i / x ] ph /\ [ j / x ] ph ) )
17 equsb3 
 |-  ( [ i / x ] x = j <-> i = j )
18 16 17 imbi12i 
 |-  ( ( [ i / x ] ( ph /\ [ j / x ] ph ) -> [ i / x ] x = j ) <-> ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )
19 10 18 bitri 
 |-  ( [ i / x ] ( ( ph /\ [ j / x ] ph ) -> x = j ) <-> ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )
20 19 sbalv 
 |-  ( [ i / x ] A. j ( ( ph /\ [ j / x ] ph ) -> x = j ) <-> A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )
21 20 albii 
 |-  ( A. i [ i / x ] A. j ( ( ph /\ [ j / x ] ph ) -> x = j ) <-> A. i A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )
22 3 9 21 3bitri 
 |-  ( E* x ph <-> A. i A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )