reu7

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006)

		Ref	Expression
	Hypothesis	rmo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	reu7	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists x \in A \forall y \in A (ψ \to x = y))$

Step	Hyp	Ref	Expression
1		rmo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		reu3	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists z \in A \forall x \in A (φ \to x = z))$
3		equequ1	$⊢ x = y \to (x = z \leftrightarrow y = z)$
4		equcom	$⊢ y = z \leftrightarrow z = y$
5	3 4	bitrdi	$⊢ x = y \to (x = z \leftrightarrow z = y)$
6	1 5	imbi12d	$⊢ x = y \to ((φ \to x = z) \leftrightarrow (ψ \to z = y))$
7	6	cbvralvw	$⊢ \forall x \in A (φ \to x = z) \leftrightarrow \forall y \in A (ψ \to z = y)$
8	7	rexbii	$⊢ \exists z \in A \forall x \in A (φ \to x = z) \leftrightarrow \exists z \in A \forall y \in A (ψ \to z = y)$
9		equequ1	$⊢ z = x \to (z = y \leftrightarrow x = y)$
10	9	imbi2d	$⊢ z = x \to ((ψ \to z = y) \leftrightarrow (ψ \to x = y))$
11	10	ralbidv	$⊢ z = x \to (\forall y \in A (ψ \to z = y) \leftrightarrow \forall y \in A (ψ \to x = y))$
12	11	cbvrexvw	$⊢ \exists z \in A \forall y \in A (ψ \to z = y) \leftrightarrow \exists x \in A \forall y \in A (ψ \to x = y)$
13	8 12	bitri	$⊢ \exists z \in A \forall x \in A (φ \to x = z) \leftrightarrow \exists x \in A \forall y \in A (ψ \to x = y)$
14	13	anbi2i	$⊢ (\exists x \in A φ \land \exists z \in A \forall x \in A (φ \to x = z)) \leftrightarrow (\exists x \in A φ \land \exists x \in A \forall y \in A (ψ \to x = y))$
15	2 14	bitri	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists x \in A \forall y \in A (ψ \to x = y))$

Metamath Proof Explorer