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.

By the way, swapping x , y and ph , ps leads to an expression for E* y ps , which is equivalent to E* x ph (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without 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		df-mo	$⊢ \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	7	adantr	$⊢ (φ \land ψ) \to ((φ \to x = z) \to x = z)$
9		pm2.27	$⊢ ψ \to ((ψ \to y = z) \to y = z)$
10	9	adantl	$⊢ (φ \land ψ) \to ((ψ \to y = z) \to y = z)$
11	8 10	anim12d	$⊢ (φ \land ψ) \to (((φ \to x = z) \land (ψ \to y = z)) \to (x = z \land y = z))$
12		equtr2	$⊢ (x = z \land y = z) \to x = y$
13	11 12	syl6com	$⊢ ((φ \to x = z) \land (ψ \to y = z)) \to ((φ \land ψ) \to x = y)$
14	13	ex	$⊢ (φ \to x = z) \to ((ψ \to y = z) \to ((φ \land ψ) \to x = y))$
15	14	alimdv	$⊢ (φ \to x = z) \to (\forall y (ψ \to y = z) \to \forall y ((φ \land ψ) \to x = y))$
16	15	com12	$⊢ \forall y (ψ \to y = z) \to ((φ \to x = z) \to \forall y ((φ \land ψ) \to x = y))$
17	16	alimdv	$⊢ \forall y (ψ \to y = z) \to (\forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y))$
18	6 17	mpcom	$⊢ \forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y)$
19	18	exlimiv	$⊢ \exists z \forall x (φ \to x = z) \to \forall x \forall y ((φ \land ψ) \to x = y)$
20	2 19	sylbi	$⊢ \exists^{*} x φ \to \forall x \forall y ((φ \land ψ) \to x = y)$
21	1	cbvexvw	$⊢ \exists x φ \leftrightarrow \exists y ψ$
22	21	biimpri	$⊢ \exists y ψ \to \exists x φ$
23		ax6evr	$⊢ \exists z x = z$
24		pm3.2	$⊢ φ \to (ψ \to (φ \land ψ))$
25	24	imim1d	$⊢ φ \to (((φ \land ψ) \to x = y) \to (ψ \to x = y))$
26		ax7	$⊢ x = y \to (x = z \to y = z)$
27	25 26	syl8	$⊢ φ \to (((φ \land ψ) \to x = y) \to (ψ \to (x = z \to y = z)))$
28	27	com4r	$⊢ x = z \to (φ \to (((φ \land ψ) \to x = y) \to (ψ \to y = z)))$
29	28	impcom	$⊢ (φ \land x = z) \to (((φ \land ψ) \to x = y) \to (ψ \to y = z))$
30	29	alimdv	$⊢ (φ \land x = z) \to (\forall y ((φ \land ψ) \to x = y) \to \forall y (ψ \to y = z))$
31	30	impancom	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to (x = z \to \forall y (ψ \to y = z))$
32	31	eximdv	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to (\exists z x = z \to \exists z \forall y (ψ \to y = z))$
33	23 32	mpi	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to \exists z \forall y (ψ \to y = z)$
34		df-mo	$⊢ \exists^{*} y ψ \leftrightarrow \exists z \forall y (ψ \to y = z)$
35	33 34	sylibr	$⊢ (φ \land \forall y ((φ \land ψ) \to x = y)) \to \exists^{*} y ψ$
36	35	expcom	$⊢ \forall y ((φ \land ψ) \to x = y) \to (φ \to \exists^{*} y ψ)$
37	36	aleximi	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to (\exists x φ \to \exists x \exists^{*} y ψ)$
38		ax5e	$⊢ \exists x \exists^{} y ψ \to \exists^{} y ψ$
39	22 37 38	syl56	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to (\exists y ψ \to \exists^{*} y ψ)$
40	5	exbii	$⊢ \exists z \forall x (φ \to x = z) \leftrightarrow \exists z \forall y (ψ \to y = z)$
41	40 2 34	3bitr4i	$⊢ \exists^{} x φ \leftrightarrow \exists^{} y ψ$
42		moabs	$⊢ \exists^{} y ψ \leftrightarrow (\exists y ψ \to \exists^{} y ψ)$
43	41 42	bitri	$⊢ \exists^{} x φ \leftrightarrow (\exists y ψ \to \exists^{} y ψ)$
44	39 43	sylibr	$⊢ \forall x \forall y ((φ \land ψ) \to x = y) \to \exists^{*} x φ$
45	20 44	impbii	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land ψ) \to x = y)$

Metamath Proof Explorer

Theorem mo4

Proof