rmo3f

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

	Ref	Expression
Hypotheses	rmo3f.1	$⊢ \underline{Ⅎ} x A$
	rmo3f.2	$⊢ \underline{Ⅎ} y A$
	rmo3f.3	$⊢ Ⅎ y φ$
Assertion	rmo3f	$⊢ \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		rmo3f.1	$⊢ \underline{Ⅎ} x A$
2		rmo3f.2	$⊢ \underline{Ⅎ} y A$
3		rmo3f.3	$⊢ Ⅎ y φ$
4		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
5		sban	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow ([y/ x] x \in A \land [y/ x] φ)$
6	1	clelsb1fw	$⊢ [y/ x] x \in A \leftrightarrow y \in A$
7	6	anbi1i	$⊢ ([y/ x] x \in A \land [y/ x] φ) \leftrightarrow (y \in A \land [y/ x] φ)$
8	5 7	bitri	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ)$
9	8	anbi2i	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((x \in A \land φ) \land (y \in A \land [y/ x] φ))$
10		an4	$⊢ ((x \in A \land φ) \land (y \in A \land [y/ x] φ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land [y/ x] φ))$
11		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
12	11	anbi1i	$⊢ ((x \in A \land y \in A) \land (φ \land [y/ x] φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
13	9 10 12	3bitri	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land [y/ x] φ))$
14	13	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)$
15		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))$
16		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)))$
17	14 15 16	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)))$
18	17	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)))$
19		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)))$
20	2	nfcri	$⊢ Ⅎ y x \in A$
21	20	r19.21	$⊢ \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))$
22	18 19 21	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))$
23	22	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))$
24	20 3	nfan	$⊢ Ⅎ y (x \in A \land φ)$
25	24	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)$
26		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))$
27	23 25 26	3bitr4i	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$
28	4 27	bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$

Metamath Proof Explorer

Theorem rmo3f

Proof