mo5f

Description: Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017)

	Ref	Expression
Hypotheses	mo5f.1	$⊢ Ⅎ i φ$
	mo5f.2	$⊢ Ⅎ j φ$
Assertion	mo5f	$⊢ \exists^{*} x φ \leftrightarrow \forall i \forall j (([i/ x] φ \land [j/ x] φ) \to i = j)$

Proof

Step	Hyp	Ref	Expression
1		mo5f.1	$⊢ Ⅎ i φ$
2		mo5f.2	$⊢ Ⅎ j φ$
3	2	mo3	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall j ((φ \land [j/ x] φ) \to x = j)$
4	1	nfsbv	$⊢ Ⅎ i [j/ x] φ$
5	1 4	nfan	$⊢ Ⅎ i (φ \land [j/ x] φ)$
6		nfv	$⊢ Ⅎ i x = j$
7	5 6	nfim	$⊢ Ⅎ i ((φ \land [j/ x] φ) \to x = j)$
8	7	nfal	$⊢ Ⅎ i \forall j ((φ \land [j/ x] φ) \to x = j)$
9	8	sb8f	$⊢ \forall x \forall j ((φ \land [j/ x] φ) \to x = j) \leftrightarrow \forall i [i/ x] \forall j ((φ \land [j/ x] φ) \to x = j)$
10		sbim	$⊢ [i/ x] ((φ \land [j/ x] φ) \to x = j) \leftrightarrow ([i/ x] (φ \land [j/ x] φ) \to [i/ x] x = j)$
11		sban	$⊢ [i/ x] (φ \land [j/ x] φ) \leftrightarrow ([i/ x] φ \land [i/ x] [j/ x] φ)$
12		nfs1v	$⊢ Ⅎ x [j/ x] φ$
13	12	sbf	$⊢ [i/ x] [j/ x] φ \leftrightarrow [j/ x] φ$
14	13	bicomi	$⊢ [j/ x] φ \leftrightarrow [i/ x] [j/ x] φ$
15	14	anbi2i	$⊢ ([i/ x] φ \land [j/ x] φ) \leftrightarrow ([i/ x] φ \land [i/ x] [j/ x] φ)$
16	11 15	bitr4i	$⊢ [i/ x] (φ \land [j/ x] φ) \leftrightarrow ([i/ x] φ \land [j/ x] φ)$
17		equsb3	$⊢ [i/ x] x = j \leftrightarrow i = j$
18	16 17	imbi12i	$⊢ ([i/ x] (φ \land [j/ x] φ) \to [i/ x] x = j) \leftrightarrow (([i/ x] φ \land [j/ x] φ) \to i = j)$
19	10 18	bitri	$⊢ [i/ x] ((φ \land [j/ x] φ) \to x = j) \leftrightarrow (([i/ x] φ \land [j/ x] φ) \to i = j)$
20	19	sbalv	$⊢ [i/ x] \forall j ((φ \land [j/ x] φ) \to x = j) \leftrightarrow \forall j (([i/ x] φ \land [j/ x] φ) \to i = j)$
21	20	albii	$⊢ \forall i [i/ x] \forall j ((φ \land [j/ x] φ) \to x = j) \leftrightarrow \forall i \forall j (([i/ x] φ \land [j/ x] φ) \to i = j)$
22	3 9 21	3bitri	$⊢ \exists^{*} x φ \leftrightarrow \forall i \forall j (([i/ x] φ \land [j/ x] φ) \to i = j)$

Metamath Proof Explorer

Theorem mo5f

Proof