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	3 4	bianbi	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ)$
6	5	anbi2i	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((x \in A \land φ) \land (y \in A \land [y/ x] φ))$
7		an4	$⊢ ((x \in A \land φ) \land (y \in A \land [y/ x] φ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land [y/ x] φ))$
8		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
9	8	anbi1i	$⊢ ((x \in A \land y \in A) \land (φ \land [y/ x] φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
10	6 7 9	3bitri	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
11	10	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)$
12		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))$
13		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)))$
14	11 12 13	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)))$
15	14	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)))$
16		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)))$
17		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))$
18	15 16 17	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))$
19	18	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))$
20		nfv	$⊢ Ⅎ y x \in A$
21	20 1	nfan	$⊢ Ⅎ y (x \in A \land φ)$
22	21	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)$
23		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))$
24	19 22 23	3bitr4i	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$
25	2 24	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