reu8

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

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

Proof

Step	Hyp	Ref	Expression
1		rmo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2	1	cbvreuvw	$⊢ \exists! x \in A φ \leftrightarrow \exists! y \in A ψ$
3		reu6	$⊢ \exists! y \in A ψ \leftrightarrow \exists x \in A \forall y \in A (ψ \leftrightarrow y = x)$
4		dfbi2	$⊢ (ψ \leftrightarrow y = x) \leftrightarrow ((ψ \to y = x) \land (y = x \to ψ))$
5	4	ralbii	$⊢ \forall y \in A (ψ \leftrightarrow y = x) \leftrightarrow \forall y \in A ((ψ \to y = x) \land (y = x \to ψ))$
6		r19.26	$⊢ \forall y \in A ((ψ \to y = x) \land (y = x \to ψ)) \leftrightarrow (\forall y \in A (ψ \to y = x) \land \forall y \in A (y = x \to ψ))$
7		ancom	$⊢ (φ \land \forall y \in A (ψ \to x = y)) \leftrightarrow (\forall y \in A (ψ \to x = y) \land φ)$
8		equcom	$⊢ x = y \leftrightarrow y = x$
9	8	imbi2i	$⊢ (ψ \to x = y) \leftrightarrow (ψ \to y = x)$
10	9	ralbii	$⊢ \forall y \in A (ψ \to x = y) \leftrightarrow \forall y \in A (ψ \to y = x)$
11	10	a1i	$⊢ x \in A \to (\forall y \in A (ψ \to x = y) \leftrightarrow \forall y \in A (ψ \to y = x))$
12		biimt	$⊢ x \in A \to (φ \leftrightarrow (x \in A \to φ))$
13		df-ral	$⊢ \forall y \in A (y = x \to ψ) \leftrightarrow \forall y (y \in A \to (y = x \to ψ))$
14		bi2.04	$⊢ (y \in A \to (y = x \to ψ)) \leftrightarrow (y = x \to (y \in A \to ψ))$
15	14	albii	$⊢ \forall y (y \in A \to (y = x \to ψ)) \leftrightarrow \forall y (y = x \to (y \in A \to ψ))$
16		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
17	16 1	imbi12d	$⊢ x = y \to ((x \in A \to φ) \leftrightarrow (y \in A \to ψ))$
18	17	bicomd	$⊢ x = y \to ((y \in A \to ψ) \leftrightarrow (x \in A \to φ))$
19	18	equcoms	$⊢ y = x \to ((y \in A \to ψ) \leftrightarrow (x \in A \to φ))$
20	19	equsalvw	$⊢ \forall y (y = x \to (y \in A \to ψ)) \leftrightarrow (x \in A \to φ)$
21	13 15 20	3bitrri	$⊢ (x \in A \to φ) \leftrightarrow \forall y \in A (y = x \to ψ)$
22	12 21	bitrdi	$⊢ x \in A \to (φ \leftrightarrow \forall y \in A (y = x \to ψ))$
23	11 22	anbi12d	$⊢ x \in A \to ((\forall y \in A (ψ \to x = y) \land φ) \leftrightarrow (\forall y \in A (ψ \to y = x) \land \forall y \in A (y = x \to ψ)))$
24	7 23	bitrid	$⊢ x \in A \to ((φ \land \forall y \in A (ψ \to x = y)) \leftrightarrow (\forall y \in A (ψ \to y = x) \land \forall y \in A (y = x \to ψ)))$
25	6 24	bitr4id	$⊢ x \in A \to (\forall y \in A ((ψ \to y = x) \land (y = x \to ψ)) \leftrightarrow (φ \land \forall y \in A (ψ \to x = y)))$
26	5 25	bitrid	$⊢ x \in A \to (\forall y \in A (ψ \leftrightarrow y = x) \leftrightarrow (φ \land \forall y \in A (ψ \to x = y)))$
27	26	rexbiia	$⊢ \exists x \in A \forall y \in A (ψ \leftrightarrow y = x) \leftrightarrow \exists x \in A (φ \land \forall y \in A (ψ \to x = y))$
28	2 3 27	3bitri	$⊢ \exists! x \in A φ \leftrightarrow \exists x \in A (φ \land \forall y \in A (ψ \to x = y))$

Metamath Proof Explorer

Theorem reu8

Proof