Metamath Proof Explorer

Theorem reusv1

Description: Two ways to express single-valuedness of a class expression C ( y ) . (Contributed by NM, 16-Dec-2012) (Proof shortened by Mario Carneiro, 18-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

		Ref	Expression
	Assertion	reusv1	$⊢ \exists y \in B φ \to (\exists! x \in A \forall y \in B (φ \to x = C) \leftrightarrow \exists x \in A \forall y \in B (φ \to x = C))$

Proof

Step	Hyp	Ref	Expression
1		nfra1	$⊢ Ⅎ y \forall y \in B (φ \to x = C)$
2	1	nfmov	$⊢ Ⅎ y \exists^{*} x \forall y \in B (φ \to x = C)$
3		rsp	$⊢ \forall y \in B (φ \to x = C) \to (y \in B \to (φ \to x = C))$
4	3	com3l	$⊢ y \in B \to (φ \to (\forall y \in B (φ \to x = C) \to x = C))$
5	4	alrimdv	$⊢ y \in B \to (φ \to \forall x (\forall y \in B (φ \to x = C) \to x = C))$
6		mo2icl	$⊢ \forall x (\forall y \in B (φ \to x = C) \to x = C) \to \exists^{*} x \forall y \in B (φ \to x = C)$
7	5 6	syl6	$⊢ y \in B \to (φ \to \exists^{*} x \forall y \in B (φ \to x = C))$
8	2 7	rexlimi	$⊢ \exists y \in B φ \to \exists^{*} x \forall y \in B (φ \to x = C)$
9		mormo	$⊢ \exists^{} x \forall y \in B (φ \to x = C) \to \exists^{} x \in A \forall y \in B (φ \to x = C)$
10		reu5	$⊢ \exists! x \in A \forall y \in B (φ \to x = C) \leftrightarrow (\exists x \in A \forall y \in B (φ \to x = C) \land \exists^{*} x \in A \forall y \in B (φ \to x = C))$
11	10	rbaib	$⊢ \exists^{*} x \in A \forall y \in B (φ \to x = C) \to (\exists! x \in A \forall y \in B (φ \to x = C) \leftrightarrow \exists x \in A \forall y \in B (φ \to x = C))$
12	8 9 11	3syl	$⊢ \exists y \in B φ \to (\exists! x \in A \forall y \in B (φ \to x = C) \leftrightarrow \exists x \in A \forall y \in B (φ \to x = C))$