rmo3

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) Avoid ax-13 . (Revised by Wolf Lammen, 30-Apr-2023)

		Ref	Expression
	Hypothesis	rmo2.1	$⊢ Ⅎ y φ$
	Assertion	rmo3	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	$⊢ Ⅎ y φ$
2		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
3		sban	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow ([y/ x] x \in A \land [y/ x] φ)$
4		clelsb1	$⊢ [y/ x] x \in A \leftrightarrow y \in A$
5	4	anbi1i	$⊢ ([y/ x] x \in A \land [y/ x] φ) \leftrightarrow (y \in A \land [y/ x] φ)$
6	3 5	bitri	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ)$
7	6	anbi2i	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((x \in A \land φ) \land (y \in A \land [y/ x] φ))$
8		an4	$⊢ ((x \in A \land φ) \land (y \in A \land [y/ x] φ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land [y/ x] φ))$
9		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
10	9	anbi1i	$⊢ ((x \in A \land y \in A) \land (φ \land [y/ x] φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
11	7 8 10	3bitri	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
12	11	imbi1i	$⊢ (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (((y \in A \land x \in A) \land (φ \land [y/ x] φ)) \to x = y)$
13		impexp	$⊢ (((y \in A \land x \in A) \land (φ \land [y/ x] φ)) \to x = y) \leftrightarrow ((y \in A \land x \in A) \to ((φ \land [y/ x] φ) \to x = y))$
14		impexp	$⊢ ((y \in A \land x \in A) \to ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow (y \in A \to (x \in A \to ((φ \land [y/ x] φ) \to x = y)))$
15	12 13 14	3bitri	$⊢ (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (y \in A \to (x \in A \to ((φ \land [y/ x] φ) \to x = y)))$
16	15	albii	$⊢ \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow \forall y (y \in A \to (x \in A \to ((φ \land [y/ x] φ) \to x = y)))$
17		df-ral	$⊢ \forall y \in A (x \in A \to ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow \forall y (y \in A \to (x \in A \to ((φ \land [y/ x] φ) \to x = y)))$
18		r19.21v	$⊢ \forall y \in A (x \in A \to ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
19	16 17 18	3bitr2i	$⊢ \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
20	19	albii	$⊢ \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
21		nfv	$⊢ Ⅎ y x \in A$
22	21 1	nfan	$⊢ Ⅎ y (x \in A \land φ)$
23	22	mo3	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y)$
24		df-ral	$⊢ \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
25	20 23 24	3bitr4i	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$
26	2 25	bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$

Metamath Proof Explorer

Theorem rmo3

Proof