CINXE.COM
df-eu - Metamath Proof Explorer
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <HTML LANG="EN-US"> <HEAD> <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> <META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0"> <STYLE TYPE="text/css"> <!-- img { margin-bottom: -4px } .r { font-family: "Arial Narrow"; font-size: x-small; } .i { font-family: "Arial Narrow"; font-size: x-small; color: gray; } --> </STYLE> <STYLE TYPE="text/css"> <!-- .setvar { color: red; } .wff { color: blue; } .class { color: #C3C; } .symvar { border-bottom:1px dotted;color:#C3C} .typecode { color: gray } .hidden { color: gray } @font-face { font-family: XITSMath-Regular; src: url(xits-math.woff); } .math { font-family: XITSMath-Regular } --> </STYLE> <LINK href="mmset.css" title="mmset" rel="stylesheet" type="text/css"> <LINK href="mmsetalt.css" title="mmsetalt" rel="alternate stylesheet" type="text/css"> <TITLE>df-eu - Metamath Proof Explorer</TITLE> <LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon"> </HEAD> <BODY BGCOLOR="#FFFFFF"> <TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%"> <TR> <TD ALIGN=LEFT VALIGN=TOP WIDTH="25%"><A HREF= "mmset.html"><IMG SRC="mm.gif" BORDER=0 ALT="MPE Home" TITLE="MPE Home" HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A> </TD> <TD ALIGN=CENTER COLSPAN=2 VALIGN=TOP><FONT SIZE="+3" COLOR="#006633"><B> Metamath Proof Explorer </B></FONT></TD> <TD ALIGN=RIGHT VALIGN=TOP WIDTH="25%"> <FONT SIZE=-1 FACE=sans-serif> <A HREF="weu.html"> < Previous</A> <A HREF="eu3v.html">Next ></A> </FONT><FONT FACE=sans-serif SIZE=-2> <BR><A HREF="mmtheorems26.html#df-eu">Nearby theorems</A> </FONT> </TD> </TR> <TR> <TD COLSPAN=2 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2 FACE=sans-serif> <A HREF="../mm.html">Mirrors</A> > <A HREF="../index.html">Home</A> > <A HREF="mmset.html">MPE Home</A> > <A HREF="mmtheorems.html">Th. List</A> > df-eu </FONT> </TD> <TD COLSPAN=2 ALIGN=RIGHT VALIGN=TOP> <FONT SIZE=-2 FACE=sans-serif> <A HREF="http://metamath.tirix.org/mpests/df-eu.html">Structured version</A> <A HREF="https://expln.github.io/metamath/asrt/df-eu.html">Visualization version</A> <A HREF="../mpegif/df-eu.html">GIF version</A> </FONT> </TD> </TR> </TABLE> <HR NOSHADE SIZE=1> <CENTER><B><FONT SIZE="+1">Definition <FONT COLOR="#006633">df-eu</FONT></FONT></B> <SPAN CLASS=r STYLE="color:#F21D00">2568</SPAN></CENTER> <CENTER><TABLE><TR><TD ALIGN=LEFT><B>Description: </B>Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (<A HREF="df-ex.html">df-ex</A> <SPAN CLASS=r STYLE="color:#F60E00">1784</SPAN>) and uniqueness (<A HREF="df-mo.html">df-mo</A> <SPAN CLASS=r STYLE="color:#F21C00">2539</SPAN>). The expression <SPAN CLASS=math>∃!<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN> is read "there exists exactly one <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN></SPAN> such that <SPAN CLASS=math><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN> " or "there exists a unique <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN></SPAN> such that <SPAN CLASS=math><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN>". This is also called the "uniqueness quantifier" but that expression is also used for the at-most-one quantifier <A HREF="df-mo.html">df-mo</A> <SPAN CLASS=r STYLE="color:#F21C00">2539</SPAN>, therefore we avoid that ambiguous name. <P STYLE="margin-bottom:0em"> Definition 10.1 of [<A HREF="mmset.html#BellMachover">BellMachover</A>] p. 97; also Definition *14.02 of [<A HREF="mmset.html#WhiteheadRussell">WhiteheadRussell</A>] p. 175. Other possible definitions are given by <A HREF="eu1.html">eu1</A> <SPAN CLASS=r STYLE="color:#F11E00">2611</SPAN>, <A HREF="eu2.html">eu2</A> <SPAN CLASS=r STYLE="color:#F11E00">2610</SPAN>, <A HREF="eu3v.html">eu3v</A> <SPAN CLASS=r STYLE="color:#F21D00">2569</SPAN>, and <A HREF="eu6.html">eu6</A> <SPAN CLASS=r STYLE="color:#F21D00">2573</SPAN>. As for double unique existence, beware that the expression <SPAN CLASS=math>∃!<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN>∃!<SPAN CLASS=setvar STYLE="color:red">𝑦</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN> means "there exists a unique <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN></SPAN> such that there exists a unique <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑦</SPAN></SPAN> such that <SPAN CLASS=math><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN> " which is a weaker property than "there exists exactly one <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN></SPAN> and one <SPAN CLASS=math><SPAN CLASS=setvar STYLE="color:red">𝑦</SPAN></SPAN> such that <SPAN CLASS=math><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN> " (see <A HREF="2eu4.html">2eu4</A> <SPAN CLASS=r STYLE="color:#F11F00">2655</SPAN>). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be <A HREF="eu6.html">eu6</A> <SPAN CLASS=r STYLE="color:#F21D00">2573</SPAN>, while this definition was then proved as <A HREF="dfeu.html">dfeu</A> <SPAN CLASS=r STYLE="color:#F11E00">2594</SPAN>). (Revised by BJ, 30-Sep-2022.)</TD></TR></TABLE></CENTER> <CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" SUMMARY="Assertion"> <CAPTION><B>Assertion</B></CAPTION> <TR><TH>Ref </TH><TH>Expression</TH></TR> <TR ALIGN=LEFT><TD><FONT COLOR="#006633"><B>df-eu</B></FONT></TD><TD> <SPAN CLASS=math><SPAN CLASS=hidden STYLE="color:gray">⊢ </SPAN>(∃!<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN> ↔ (∃<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN> ∧ ∃*<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN>))</SPAN></TD></TR> </TABLE></CENTER> <HR NOSHADE SIZE=1> <CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" SUMMARY="Detailed syntax breakdown of definition"> <CAPTION><B>Detailed syntax breakdown of Definition <FONT COLOR="#006633">df-eu</FONT></B></CAPTION> <TR><TH>Step</TH><TH>Hyp</TH><TH>Ref </TH><TH>Expression</TH></TR> <TR ALIGN=LEFT><TD>1</TD><TD> </TD><TD>wph</TD><TD><A NAME="1"></A> <SPAN CLASS=i>. . 3</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN></TD></TR> <TR ALIGN=LEFT><TD>2</TD><TD> </TD><TD>vx</TD><TD><A NAME="2"></A> <SPAN CLASS=i>. . 3</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">setvar </SPAN><SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN></SPAN></TD></TR> <TR ALIGN=LEFT><TD>3</TD><TD><A HREF="#1">1</A>, <A HREF="#2">2</A></TD><TD><A HREF="weu.html" TITLE="Extend wff definition to include the unique existential quantifier ('there exists a...">weu</A> <SPAN CLASS=r STYLE="color:#F21D00">2567</SPAN></TD><TD><A NAME="3"></A> <SPAN CLASS=i>. 2</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN>∃!<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN></TD></TR> <TR ALIGN=LEFT><TD>4</TD><TD><A HREF="#1">1</A>, <A HREF="#2">2</A></TD><TD><A HREF="wex.html" TITLE="Extend wff definition to include the existential quantifier ('there exists').">wex</A> <SPAN CLASS=r STYLE="color:#F60E00">1783</SPAN></TD><TD><A NAME="4"></A> <SPAN CLASS=i>. . 3</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN>∃<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN></TD></TR> <TR ALIGN=LEFT><TD>5</TD><TD><A HREF="#1">1</A>, <A HREF="#2">2</A></TD><TD><A HREF="wmo.html" TITLE="Extend wff definition to include the at-most-one quantifier ('there exists at most...">wmo</A> <SPAN CLASS=r STYLE="color:#F21C00">2537</SPAN></TD><TD><A NAME="5"></A> <SPAN CLASS=i>. . 3</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN>∃*<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN></SPAN></TD></TR> <TR ALIGN=LEFT><TD>6</TD><TD><A HREF="#4">4</A>, <A HREF="#5">5</A></TD><TD><A HREF="wa.html" TITLE="Extend wff definition to include conjunction ('and').">wa</A> <SPAN CLASS=r STYLE="color:#FA0200">395</SPAN></TD><TD><A NAME="6"></A> <SPAN CLASS=i>. 2</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN>(∃<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN> ∧ ∃*<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN>)</SPAN></TD></TR> <TR ALIGN=LEFT><TD>7</TD><TD><A HREF="#3">3</A>, <A HREF="#6">6</A></TD><TD><A HREF="wb.html" TITLE="Extend wff definition to include the biconditional connective.">wb</A> <SPAN CLASS=r STYLE="color:#FA0100">205</SPAN></TD><TD><A NAME="7"></A> <SPAN CLASS=i>1</SPAN> <SPAN CLASS=math><SPAN CLASS=typecode STYLE="color:gray">wff </SPAN>(∃!<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN> ↔ (∃<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN> ∧ ∃*<SPAN CLASS=setvar STYLE="color:red">𝑥</SPAN><SPAN CLASS=wff STYLE="color:blue">𝜑</SPAN>))</SPAN></TD></TR> </TABLE></CENTER> <CENTER><TABLE CELLSPACING=5><TR><TD ALIGN=LEFT><FONT SIZE=-1><B>Colors of variables:</B> <SPAN CLASS=wff STYLE="color:blue;font-style:normal">wff</SPAN> <SPAN CLASS=setvar STYLE="color:red;font-style:normal">setvar</SPAN> <SPAN CLASS=class STYLE="color:#C3C;font-style:normal">class</SPAN></FONT></TD></TR> <TR><TD ALIGN=LEFT><FONT SIZE=-1><B>This definition is referenced by:</B> <A HREF="eu3v.html">eu3v</A> <SPAN CLASS=r STYLE="color:#F21D00">2569</SPAN> <A HREF="euex.html">euex</A> <SPAN CLASS=r STYLE="color:#F21D00">2576</SPAN> <A HREF="eumo.html">eumo</A> <SPAN CLASS=r STYLE="color:#F21D00">2577</SPAN> <A HREF="exmoeub.html">exmoeub</A> <SPAN CLASS=r STYLE="color:#F21D00">2579</SPAN> <A HREF="moeuex.html">moeuex</A> <SPAN CLASS=r STYLE="color:#F11D00">2581</SPAN> <A HREF="eubi.html">eubi</A> <SPAN CLASS=r STYLE="color:#F11D00">2583</SPAN> <A HREF="eubii.html">eubii</A> <SPAN CLASS=r STYLE="color:#F11D00">2584</SPAN> <A HREF="nfeu1ALT.html">nfeu1ALT</A> <SPAN CLASS=r STYLE="color:#F11D00">2588</SPAN> <A HREF="nfeud2.html">nfeud2</A> <SPAN CLASS=r STYLE="color:#F11D00">2589</SPAN> <A HREF="nfeudw.html">nfeudw</A> <SPAN CLASS=r STYLE="color:#F11D00">2590</SPAN> <A HREF="cbveuvw.html">cbveuvw</A> <SPAN CLASS=r STYLE="color:#F11E00">2605</SPAN> <A HREF="cbveuw.html">cbveuw</A> <SPAN CLASS=r STYLE="color:#F11E00">2606</SPAN> <A HREF="cbveuALT.html">cbveuALT</A> <SPAN CLASS=r STYLE="color:#F11E00">2609</SPAN> <A HREF="eu2.html">eu2</A> <SPAN CLASS=r STYLE="color:#F11E00">2610</SPAN> <A HREF="eu4.html">eu4</A> <SPAN CLASS=r STYLE="color:#F11E00">2616</SPAN> <A HREF="2euswapv.html">2euswapv</A> <SPAN CLASS=r STYLE="color:#F11E00">2631</SPAN> <A HREF="2euexv.html">2euexv</A> <SPAN CLASS=r STYLE="color:#F11E00">2632</SPAN> <A HREF="2exeuv.html">2exeuv</A> <SPAN CLASS=r STYLE="color:#F11E00">2633</SPAN> <A HREF="2euex.html">2euex</A> <SPAN CLASS=r STYLE="color:#F11E00">2642</SPAN> <A HREF="2euswap.html">2euswap</A> <SPAN CLASS=r STYLE="color:#F11F00">2646</SPAN> <A HREF="2exeu.html">2exeu</A> <SPAN CLASS=r STYLE="color:#F11F00">2647</SPAN> <A HREF="2eu4.html">2eu4</A> <SPAN CLASS=r STYLE="color:#F11F00">2655</SPAN> <A HREF="reu5.html">reu5</A> <SPAN CLASS=r STYLE="color:#ED2C00">3356</SPAN> <A HREF="eueq.html">eueq</A> <SPAN CLASS=r STYLE="color:#EA3100">3643</SPAN> <A HREF="reuss2.html">reuss2</A> <SPAN CLASS=r STYLE="color:#E43B00">4251</SPAN> <A HREF="n0moeu.html">n0moeu</A> <SPAN CLASS=r STYLE="color:#E43B00">4292</SPAN> <A HREF="reusv2lem1.html">reusv2lem1</A> <SPAN CLASS=r STYLE="color:#DA4A00">5321</SPAN> <A HREF="funcnv3.html">funcnv3</A> <SPAN CLASS=r STYLE="color:#CC5700">6493</SPAN> <A HREF="fnres.html">fnres</A> <SPAN CLASS=r STYLE="color:#CB5800">6548</SPAN> <A HREF="mptfnf.html">mptfnf</A> <SPAN CLASS=r STYLE="color:#CB5800">6557</SPAN> <A HREF="fnopabg.html">fnopabg</A> <SPAN CLASS=r STYLE="color:#CB5800">6559</SPAN> <A HREF="brprcneu.html">brprcneu</A> <SPAN CLASS=r STYLE="color:#C95A00">6752</SPAN> <A HREF="fvprc.html">fvprc</A> <SPAN CLASS=r STYLE="color:#C95A00">6753</SPAN> <A HREF="dff3.html">dff3</A> <SPAN CLASS=r STYLE="color:#C65C00">6963</SPAN> <A HREF="finnisoeu.html">finnisoeu</A> <SPAN CLASS=r STYLE="color:#9C7800">9809</SPAN> <A HREF="dfac2b.html">dfac2b</A> <SPAN CLASS=r STYLE="color:#9B7800">9826</SPAN> <A HREF="recmulnq.html">recmulnq</A> <SPAN CLASS=r STYLE="color:#8E7D00">10660</SPAN> <A HREF="uptx.html">uptx</A> <SPAN CLASS=r STYLE="color:#009153">22713</SPAN> <A HREF="hausflf2.html">hausflf2</A> <SPAN CLASS=r STYLE="color:#00915B">23086</SPAN> <A HREF="adjeu.html">adjeu</A> <SPAN CLASS=r STYLE="color:#107DFF">30185</SPAN> <A HREF="bnj151.html">bnj151</A> <SPAN CLASS=r STYLE="color:#656FFF">32793</SPAN> <A HREF="bnj600.html">bnj600</A> <SPAN CLASS=r STYLE="color:#666FFF">32835</SPAN> <A HREF="nosupno.html">nosupno</A> <SPAN CLASS=r STYLE="color:#7968FF">33869</SPAN> <A HREF="nosupfv.html">nosupfv</A> <SPAN CLASS=r STYLE="color:#7968FF">33872</SPAN> <A HREF="noinfno.html">noinfno</A> <SPAN CLASS=r STYLE="color:#7968FF">33884</SPAN> <A HREF="noinffv.html">noinffv</A> <SPAN CLASS=r STYLE="color:#7968FF">33887</SPAN> <A HREF="bj-eu3f.html">bj-eu3f</A> <SPAN CLASS=r STYLE="color:#8C60FF">34988</SPAN> <A HREF="wl-euae.html">wl-euae</A> <SPAN CLASS=r STYLE="color:#9858FF">35639</SPAN> <A HREF="eu0.html">eu0</A> <SPAN CLASS=r STYLE="color:#D214EE">41061</SPAN> <A HREF="fzisoeu.html">fzisoeu</A> <SPAN CLASS=r STYLE="color:#DB03E0">42765</SPAN> <A HREF="ellimciota.html">ellimciota</A> <SPAN CLASS=r STYLE="color:#DC00DE">43081</SPAN> <A HREF="euabsneu.html">euabsneu</A> <SPAN CLASS=r STYLE="color:#E600B6">44445</SPAN> <A HREF="iota0ndef.html">iota0ndef</A> <SPAN CLASS=r STYLE="color:#E600B5">44456</SPAN> <A HREF="aiota0ndef.html">aiota0ndef</A> <SPAN CLASS=r STYLE="color:#E700B4">44512</SPAN> <A HREF="reutruALT.html">reutruALT</A> <SPAN CLASS=r STYLE="color:#ED008C">46076</SPAN> <A HREF="mo0sn.html">mo0sn</A> <SPAN CLASS=r STYLE="color:#ED008C">46085</SPAN> <A HREF="thincn0eu.html">thincn0eu</A> <SPAN CLASS=r STYLE="color:#EE0088">46237</SPAN></FONT></TD></TR></TABLE></CENTER> <TABLE BORDER=0 WIDTH="100%"> <TR><TD WIDTH="25%"> </TD> <TD ALIGN=CENTER VALIGN=BOTTOM> <FONT SIZE=-2 FACE=sans-serif> Copyright terms: <A HREF="../copyright.html#pd">Public domain</A> </FONT></TD><TD ALIGN=RIGHT VALIGN=BOTTOM WIDTH="25%"> <FONT SIZE=-2 FACE=sans-serif> <A HREF="http://validator.w3.org/check?uri=referer"> W3C validator</A> </FONT></TD></TR></TABLE> </BODY></HTML>