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	$⊢ Ⅎ y φ$
	Assertion	mo3	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land [y/ x] φ) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		mo3.nf	$⊢ Ⅎ y φ$
2		nfmo1	$⊢ Ⅎ x \exists^{*} x φ$
3	1	nfmov	$⊢ Ⅎ y \exists^{*} x φ$
4		df-mo	$⊢ \exists^{*} x φ \leftrightarrow \exists z \forall x (φ \to x = z)$
5		sp	$⊢ \forall x (φ \to x = z) \to (φ \to x = z)$
6		spsbim	$⊢ \forall x (φ \to x = z) \to ([y/ x] φ \to [y/ x] x = z)$
7		equsb3	$⊢ [y/ x] x = z \leftrightarrow y = z$
8	6 7	imbitrdi	$⊢ \forall x (φ \to x = z) \to ([y/ x] φ \to y = z)$
9	5 8	anim12d	$⊢ \forall x (φ \to x = z) \to ((φ \land [y/ x] φ) \to (x = z \land y = z))$
10		equtr2	$⊢ (x = z \land y = z) \to x = y$
11	9 10	syl6	$⊢ \forall x (φ \to x = z) \to ((φ \land [y/ x] φ) \to x = y)$
12	11	exlimiv	$⊢ \exists z \forall x (φ \to x = z) \to ((φ \land [y/ x] φ) \to x = y)$
13	4 12	sylbi	$⊢ \exists^{*} x φ \to ((φ \land [y/ x] φ) \to x = y)$
14	3 13	alrimi	$⊢ \exists^{*} x φ \to \forall y ((φ \land [y/ x] φ) \to x = y)$
15	2 14	alrimi	$⊢ \exists^{*} x φ \to \forall x \forall y ((φ \land [y/ x] φ) \to x = y)$
16		nfs1v	$⊢ Ⅎ x [y/ x] φ$
17		pm3.21	$⊢ [y/ x] φ \to (φ \to (φ \land [y/ x] φ))$
18	17	imim1d	$⊢ [y/ x] φ \to (((φ \land [y/ x] φ) \to x = y) \to (φ \to x = y))$
19	16 18	alimd	$⊢ [y/ x] φ \to (\forall x ((φ \land [y/ x] φ) \to x = y) \to \forall x (φ \to x = y))$
20	19	com12	$⊢ \forall x ((φ \land [y/ x] φ) \to x = y) \to ([y/ x] φ \to \forall x (φ \to x = y))$
21	20	aleximi	$⊢ \forall y \forall x ((φ \land [y/ x] φ) \to x = y) \to (\exists y [y/ x] φ \to \exists y \forall x (φ \to x = y))$
22	1	sb8ef	$⊢ \exists x φ \leftrightarrow \exists y [y/ x] φ$
23	1	mof	$⊢ \exists^{*} x φ \leftrightarrow \exists y \forall x (φ \to x = y)$
24	21 22 23	3imtr4g	$⊢ \forall y \forall x ((φ \land [y/ x] φ) \to x = y) \to (\exists x φ \to \exists^{*} x φ)$
25		moabs	$⊢ \exists^{} x φ \leftrightarrow (\exists x φ \to \exists^{} x φ)$
26	24 25	sylibr	$⊢ \forall y \forall x ((φ \land [y/ x] φ) \to x = y) \to \exists^{*} x φ$
27	26	alcoms	$⊢ \forall x \forall y ((φ \land [y/ x] φ) \to x = y) \to \exists^{*} x φ$
28	15 27	impbii	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land [y/ x] φ) \to x = y)$

Metamath Proof Explorer

Theorem mo3

Proof