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

Metamath Proof Explorer

Theorem mo3

Description: Alternate definition of the at-most-one quantifier. Definition of BellMachover p. 460, except that definition has the side condition that y not occur in ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995) (Proof shortened by Wolf Lammen, 18-Aug-2019) Remove dependency on ax-13 . (Revised by BJ and WL, 29-Jan-2023)

Ref Expression
Hypothesis mo3.nf 
|- F/ y ph
Assertion mo3 
|- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 mo3.nf 
 |-  F/ y ph
2 nfmo1 
 |-  F/ x E* x ph
3 1 nfmov 
 |-  F/ y E* x ph
4 df-mo 
 |-  ( E* x ph <-> E. z A. x ( ph -> x = z ) )
5 sp 
 |-  ( A. x ( ph -> x = z ) -> ( ph -> x = z ) )
6 spsbim 
 |-  ( A. x ( ph -> x = z ) -> ( [ y / x ] ph -> [ y / x ] x = z ) )
7 equsb3 
 |-  ( [ y / x ] x = z <-> y = z )
8 6 7 imbitrdi 
 |-  ( A. x ( ph -> x = z ) -> ( [ y / x ] ph -> y = z ) )
9 5 8 anim12d 
 |-  ( A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> ( x = z /\ y = z ) ) )
10 equtr2 
 |-  ( ( x = z /\ y = z ) -> x = y )
11 9 10 syl6 
 |-  ( A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
12 11 exlimiv 
 |-  ( E. z A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
13 4 12 sylbi 
 |-  ( E* x ph -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
14 3 13 alrimi 
 |-  ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
15 2 14 alrimi 
 |-  ( E* x ph -> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
16 nfs1v 
 |-  F/ x [ y / x ] ph
17 pm3.21 
 |-  ( [ y / x ] ph -> ( ph -> ( ph /\ [ y / x ] ph ) ) )
18 17 imim1d 
 |-  ( [ y / x ] ph -> ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ph -> x = y ) ) )
19 16 18 alimd 
 |-  ( [ y / x ] ph -> ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> A. x ( ph -> x = y ) ) )
20 19 com12 
 |-  ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> A. x ( ph -> x = y ) ) )
21 20 aleximi 
 |-  ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
22 1 sb8ef 
 |-  ( E. x ph <-> E. y [ y / x ] ph )
23 1 mof 
 |-  ( E* x ph <-> E. y A. x ( ph -> x = y ) )
24 21 22 23 3imtr4g 
 |-  ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. x ph -> E* x ph ) )
25 moabs 
 |-  ( E* x ph <-> ( E. x ph -> E* x ph ) )
26 24 25 sylibr 
 |-  ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph )
27 26 alcoms 
 |-  ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph )
28 15 27 impbii 
 |-  ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )