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