mo4

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f , but this proof is based on fewer axioms.

Note: Swapping both x , y and ph , ps preserves the hypothesis and DV conditions, so we also have the conclusion |- ( E* y ps <-> A. y A. x ( ( ps /\ ph ) -> y = x ) ) . But under the hypothesis and DV condition, we also have |- ( E* x ph <-> E* y ps ) (that is a proof step). Therefore, since |- ( ( ph /\ ps ) <-> ( ps <-> ph ) ) ( ancom ) and |- ( x = y <-> y = x ) ( equcom ) , we obtain, still under the hypothesis and DV condition, |- ( A. x A. y ( ( ph /\ ps ) -> x = y ) <-> A. y A. x ( ( ph /\ ps ) -> x = y ) ) ; in other words, in this special case we can swap universal quantifiers as in alcom without requiring ax-11 . (Contributed by NM, 26-Jul-1995) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023)

		Ref	Expression
	Hypothesis	mo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	mo4	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land ψ) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		mo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		dfmo	$⊢ \exists^{*} x φ \leftrightarrow \exists z \forall x (φ \to x = z)$
3		equequ1	$⊢ x = y \to (x = z \leftrightarrow y = z)$
4	1 3	imbi12d	$⊢ x = y \to ((φ \to x = z) \leftrightarrow (ψ \to y = z))$
5	4	cbvalvw	$⊢ \forall x (φ \to x = z) \leftrightarrow \forall y (ψ \to y = z)$
6	5	biimpi	$⊢ \forall x (φ \to x = z) \to \forall y (ψ \to y = z)$
7		pm2.27	$⊢ φ \to ((φ \to x = z) \to x = z)$
8		pm2.27	$⊢ ψ \to ((ψ \to y = z) \to y = z)$
9	7 8	im2anan9	$⊢ (φ \land ψ) \to (((φ \to x = z) \land (ψ \to y = z)) \to (x = z \land y = z))$
10		equtr2	$⊢ (x = z \land y = z) \to x = y$
11	9 10	syl6com	$⊢ ((φ \to x = z) \land (ψ \to y = z)) \to ((φ \land ψ) \to x = y)$
12	11	ex	$⊢ (φ \to x = z) \to ((ψ \to y = z) \to ((φ \land ψ) \to x = y))$
13	12	alimdv	$⊢ (φ \to x = z) \to (\forall y (ψ \to y = z) \to \forall y ((φ \land ψ) \to x = y))$
14	13	com12	$⊢ \forall y (ψ \to y = z) \to ((φ \to x = z) \to \forall y ((φ \land ψ) \to x = y))$
15	14	alimdv	$⊢ \forall y (ψ \to y = z) \to (\forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y))$
16	6 15	mpcom	$⊢ \forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y)$
17	16	exlimiv	$⊢ \exists z \forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y)$
18	2 17	sylbi	$⊢ \exists^{*} x φ \to \forall x \forall y ((φ \land ψ) \to x = y)$
19	1	cbvexvw	$⊢ \exists x φ \leftrightarrow \exists y ψ$
20	19	biimpri	$⊢ \exists y ψ \to \exists x φ$
21		ax6evr	$⊢ \exists z x = z$
22		pm3.2	$⊢ φ \to (ψ \to (φ \land ψ))$
23	22	imim1d	$⊢ φ \to (((φ \land ψ) \to x = y) \to (ψ \to x = y))$
24		ax7	$⊢ x = y \to (x = z \to y = z)$
25	23 24	syl8	$⊢ φ \to (((φ \land ψ) \to x = y) \to (ψ \to (x = z \to y = z)))$
26	25	com4r	$⊢ x = z \to (φ \to (((φ \land ψ) \to x = y) \to (ψ \to y = z)))$
27	26	impcom	$⊢ (φ \land x = z) \to (((φ \land ψ) \to x = y) \to (ψ \to y = z))$
28	27	alimdv	$⊢ (φ \land x = z) \to (\forall y ((φ \land ψ) \to x = y) \to \forall y (ψ \to y = z))$
29	28	impancom	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to (x = z \to \forall y (ψ \to y = z))$
30	29	eximdv	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to (\exists z x = z \to \exists z \forall y (ψ \to y = z))$
31	21 30	mpi	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to \exists z \forall y (ψ \to y = z)$
32		dfmo	$⊢ \exists^{*} y ψ \leftrightarrow \exists z \forall y (ψ \to y = z)$
33	31 32	sylibr	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to \exists^{*} y ψ$
34	33	expcom	$⊢ \forall y ((φ \land ψ) \to x = y) \to (φ \to \exists^{*} y ψ)$
35	34	aleximi	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to (\exists x φ \to \exists x \exists^{*} y ψ)$
36		ax5e	$⊢ \exists x \exists^{} y ψ \to \exists^{} y ψ$
37	20 35 36	syl56	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to (\exists y ψ \to \exists^{*} y ψ)$
38	5	exbii	$⊢ \exists z \forall x (φ \to x = z) \leftrightarrow \exists z \forall y (ψ \to y = z)$
39	38 2 32	3bitr4i	$⊢ \exists^{} x φ \leftrightarrow \exists^{} y ψ$
40		moabs	$⊢ \exists^{} y ψ \leftrightarrow (\exists y ψ \to \exists^{} y ψ)$
41	39 40	bitri	$⊢ \exists^{} x φ \leftrightarrow (\exists y ψ \to \exists^{} y ψ)$
42	37 41	sylibr	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to \exists^{*} x φ$
43	18 42	impbii	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land ψ) \to x = y)$

Metamath Proof Explorer

Theorem mo4

Proof