Definition df-mo 1964

Description: Define "there exists at most one x such that ph." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2014. For another possible definition see mo4 2021. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-mo	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	wmo 1961	. 2 wff E* x ph
4	1, 2	wex 1436	. . 3 wff E. x ph
5	1, 2	weu 1960	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 104	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  nfmo1  1972  sb8mo  1974  nfmod  1977  mon  1989  eumo  1992  mobidh  1994  mobid  1995  hbmo1  1998  hbmo  1999  cbvmo  2000  eu5  2007  moabs  2009  exmodc  2010  exmonim  2011  mo2r  2012  mo3h  2013  exmoeudc  2023  2euex  2047  rmo5  2604  moeq  2812  repizf2lem  4025  funeu  5084  dffun8  5087  climmo  10906