Theorem mo3 2507

Description: Alternate definition of "at most one." 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.)

Hypothesis

Ref	Expression
mo3.1	|- F/ y ph

Assertion

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

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem mo3

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfmo1 2481	. . 3 |- F/ x E* x ph
2		mo3.1	. . . . 5 |- F/ y ph
3	2	nfmo 2487	. . . 4 |- F/ y E* x ph
4		mo2v 2477	. . . . 5 |- ( E* x ph <-> E. z A. x ( ph -> x = z ) )
5		sp 2053	. . . . . . . 8 |- ( A. x ( ph -> x = z ) -> ( ph -> x = z ) )
6		spsbim 2394	. . . . . . . . 9 |- ( A. x ( ph -> x = z ) -> ( [ y / x ] ph -> [ y / x ] x = z ) )
7		equsb3 2432	. . . . . . . . 9 |- ( [ y / x ] x = z <-> y = z )
8	6, 7	syl6ib 241	. . . . . . . 8 |- ( A. x ( ph -> x = z ) -> ( [ y / x ] ph -> y = z ) )
9	5, 8	anim12d 586	. . . . . . 7 |- ( A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> ( x = z /\ y = z ) ) )
10		equtr2 1954	. . . . . . 7 |- ( ( x = z /\ y = z ) -> x = y )
11	9, 10	syl6 35	. . . . . 6 |- ( A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
12	11	exlimiv 1858	. . . . 5 |- ( E. z A. x ( ph -> x = z ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
13	4, 12	sylbi 207	. . . 4 |- ( E* x ph -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
14	3, 13	alrimi 2082	. . 3 |- ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
15	1, 14	alrimi 2082	. 2 |- ( E* x ph -> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
16		nfs1v 2437	. . . . . . . 8 |- F/ x [ y / x ] ph
17		pm3.21 464	. . . . . . . . 9 |- ( [ y / x ] ph -> ( ph -> ( ph /\ [ y / x ] ph ) ) )
18	17	imim1d 82	. . . . . . . 8 |- ( [ y / x ] ph -> ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ph -> x = y ) ) )
19	16, 18	alimd 2081	. . . . . . 7 |- ( [ y / x ] ph -> ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> A. x ( ph -> x = y ) ) )
20	19	com12 32	. . . . . 6 |- ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> A. x ( ph -> x = y ) ) )
21	20	aleximi 1759	. . . . 5 |- ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
22	2	sb8e 2425	. . . . 5 |- ( E. x ph <-> E. y [ y / x ] ph )
23	2	mo2 2479	. . . . 5 |- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
24	21, 22, 23	3imtr4g 285	. . . 4 |- ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. x ph -> E* x ph ) )
25		moabs 2501	. . . 4 |- ( E* x ph <-> ( E. x ph -> E* x ph ) )
26	24, 25	sylibr 224	. . 3 |- ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph )
27	26	alcoms 2035	. 2 |- ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph )
28	15, 27	impbii 199	1 |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   F/wnf 1708   [wsb 1880   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475

This theorem is referenced by:  mo  2508  eu2  2509  mo4f  2516  2mo  2551  rmo3  3528  isarep2  5978  mo5f  29324  rmo3f  29335  rmo4fOLD  29336  bnj580  30983  pm14.12  38622