Metamath Proof Explorer

Theorem rmo4f

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by Thierry Arnoux, 11-Oct-2016) (Revised by Thierry Arnoux, 8-Mar-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

		Ref	Expression
	Hypotheses	rmo4f.1	$⊢ \underline{Ⅎ} x A$
		rmo4f.2	$⊢ \underline{Ⅎ} y A$
		rmo4f.3	$⊢ Ⅎ x ψ$
		rmo4f.4	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	rmo4f	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		rmo4f.1	$⊢ \underline{Ⅎ} x A$
2		rmo4f.2	$⊢ \underline{Ⅎ} y A$
3		rmo4f.3	$⊢ Ⅎ x ψ$
4		rmo4f.4	$⊢ x = y \to (φ \leftrightarrow ψ)$
5		nfv	$⊢ Ⅎ y φ$
6	1 2 5	rmo3f	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)$
7	3 4	sbiev	$⊢ [y/ x] φ \leftrightarrow ψ$
8	7	anbi2i	$⊢ (φ \land [y/ x] φ) \leftrightarrow (φ \land ψ)$
9	8	imbi1i	$⊢ ((φ \land [y/ x] φ) \to x = y) \leftrightarrow ((φ \land ψ) \to x = y)$
10	9	2ralbii	$⊢ \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$
11	6 10	bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$