rmo2

Description: Alternate definition of restricted "at most one". Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

		Ref	Expression
	Hypothesis	rmo2.1	$⊢ Ⅎ y φ$
	Assertion	rmo2	$⊢ \exists^{*} x \in A φ \leftrightarrow \exists y \forall x \in A (φ \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		nfv	$⊢ Ⅎ y x \in A$
4	3 1	nfan	$⊢ Ⅎ y (x \in A \land φ)$
5	4	mof	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \exists y \forall x ((x \in A \land φ) \to x = y)$
6		impexp	$⊢ ((x \in A \land φ) \to x = y) \leftrightarrow (x \in A \to (φ \to x = y))$
7	6	albii	$⊢ \forall x ((x \in A \land φ) \to x = y) \leftrightarrow \forall x (x \in A \to (φ \to x = y))$
8		df-ral	$⊢ \forall x \in A (φ \to x = y) \leftrightarrow \forall x (x \in A \to (φ \to x = y))$
9	7 8	bitr4i	$⊢ \forall x ((x \in A \land φ) \to x = y) \leftrightarrow \forall x \in A (φ \to x = y)$
10	9	exbii	$⊢ \exists y \forall x ((x \in A \land φ) \to x = y) \leftrightarrow \exists y \forall x \in A (φ \to x = y)$
11	2 5 10	3bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \exists y \forall x \in A (φ \to x = y)$

Metamath Proof Explorer

Theorem rmo2

Proof