reuind

Description: Existential uniqueness via an indirect equality. (Contributed by NM, 16-Oct-2010)

	Ref	Expression
Hypotheses	reuind.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	reuind.2	$⊢ x = y \to A = B$
Assertion	reuind	$⊢ (\forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \land \exists x (A \in C \land φ)) \to \exists! z \in C \forall x ((A \in C \land φ) \to z = A)$

Proof

Step	Hyp	Ref	Expression
1		reuind.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		reuind.2	$⊢ x = y \to A = B$
3	2	eleq1d	$⊢ x = y \to (A \in C \leftrightarrow B \in C)$
4	3 1	anbi12d	$⊢ x = y \to ((A \in C \land φ) \leftrightarrow (B \in C \land ψ))$
5	4	cbvexvw	$⊢ \exists x (A \in C \land φ) \leftrightarrow \exists y (B \in C \land ψ)$
6		r19.41v	$⊢ \exists z \in C (z = B \land ψ) \leftrightarrow (\exists z \in C z = B \land ψ)$
7	6	exbii	$⊢ \exists y \exists z \in C (z = B \land ψ) \leftrightarrow \exists y (\exists z \in C z = B \land ψ)$
8		rexcom4	$⊢ \exists z \in C \exists y (z = B \land ψ) \leftrightarrow \exists y \exists z \in C (z = B \land ψ)$
9		risset	$⊢ B \in C \leftrightarrow \exists z \in C z = B$
10	9	anbi1i	$⊢ (B \in C \land ψ) \leftrightarrow (\exists z \in C z = B \land ψ)$
11	10	exbii	$⊢ \exists y (B \in C \land ψ) \leftrightarrow \exists y (\exists z \in C z = B \land ψ)$
12	7 8 11	3bitr4ri	$⊢ \exists y (B \in C \land ψ) \leftrightarrow \exists z \in C \exists y (z = B \land ψ)$
13	5 12	bitri	$⊢ \exists x (A \in C \land φ) \leftrightarrow \exists z \in C \exists y (z = B \land ψ)$
14		eqeq2	$⊢ A = B \to (z = A \leftrightarrow z = B)$
15	14	imim2i	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = A \leftrightarrow z = B))$
16		biimpr	$⊢ (z = A \leftrightarrow z = B) \to (z = B \to z = A)$
17	16	imim2i	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = A \leftrightarrow z = B)) \to (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = B \to z = A))$
18		an31	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \land z = B) \leftrightarrow ((z = B \land (B \in C \land ψ)) \land (A \in C \land φ))$
19	18	imbi1i	$⊢ ((((A \in C \land φ) \land (B \in C \land ψ)) \land z = B) \to z = A) \leftrightarrow (((z = B \land (B \in C \land ψ)) \land (A \in C \land φ)) \to z = A)$
20		impexp	$⊢ ((((A \in C \land φ) \land (B \in C \land ψ)) \land z = B) \to z = A) \leftrightarrow (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = B \to z = A))$
21		impexp	$⊢ (((z = B \land (B \in C \land ψ)) \land (A \in C \land φ)) \to z = A) \leftrightarrow ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
22	19 20 21	3bitr3i	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = B \to z = A)) \leftrightarrow ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
23	17 22	sylib	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \to (z = A \leftrightarrow z = B)) \to ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
24	15 23	syl	$⊢ (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
25	24	2alimi	$⊢ \forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to \forall x \forall y ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
26		19.23v	$⊢ \forall y ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow (\exists y (z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A))$
27		an12	$⊢ (z = B \land (B \in C \land ψ)) \leftrightarrow (B \in C \land (z = B \land ψ))$
28		eleq1	$⊢ z = B \to (z \in C \leftrightarrow B \in C)$
29	28	adantr	$⊢ (z = B \land ψ) \to (z \in C \leftrightarrow B \in C)$
30	29	pm5.32ri	$⊢ (z \in C \land (z = B \land ψ)) \leftrightarrow (B \in C \land (z = B \land ψ))$
31	27 30	bitr4i	$⊢ (z = B \land (B \in C \land ψ)) \leftrightarrow (z \in C \land (z = B \land ψ))$
32	31	exbii	$⊢ \exists y (z = B \land (B \in C \land ψ)) \leftrightarrow \exists y (z \in C \land (z = B \land ψ))$
33		19.42v	$⊢ \exists y (z \in C \land (z = B \land ψ)) \leftrightarrow (z \in C \land \exists y (z = B \land ψ))$
34	32 33	bitri	$⊢ \exists y (z = B \land (B \in C \land ψ)) \leftrightarrow (z \in C \land \exists y (z = B \land ψ))$
35	34	imbi1i	$⊢ (\exists y (z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow ((z \in C \land \exists y (z = B \land ψ)) \to ((A \in C \land φ) \to z = A))$
36	26 35	bitri	$⊢ \forall y ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow ((z \in C \land \exists y (z = B \land ψ)) \to ((A \in C \land φ) \to z = A))$
37	36	albii	$⊢ \forall x \forall y ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow \forall x ((z \in C \land \exists y (z = B \land ψ)) \to ((A \in C \land φ) \to z = A))$
38		19.21v	$⊢ \forall x ((z \in C \land \exists y (z = B \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow ((z \in C \land \exists y (z = B \land ψ)) \to \forall x ((A \in C \land φ) \to z = A))$
39	37 38	bitri	$⊢ \forall x \forall y ((z = B \land (B \in C \land ψ)) \to ((A \in C \land φ) \to z = A)) \leftrightarrow ((z \in C \land \exists y (z = B \land ψ)) \to \forall x ((A \in C \land φ) \to z = A))$
40	25 39	sylib	$⊢ \forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to ((z \in C \land \exists y (z = B \land ψ)) \to \forall x ((A \in C \land φ) \to z = A))$
41	40	expd	$⊢ \forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to (z \in C \to (\exists y (z = B \land ψ) \to \forall x ((A \in C \land φ) \to z = A)))$
42	41	reximdvai	$⊢ \forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to (\exists z \in C \exists y (z = B \land ψ) \to \exists z \in C \forall x ((A \in C \land φ) \to z = A))$
43	13 42	syl5bi	$⊢ \forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \to (\exists x (A \in C \land φ) \to \exists z \in C \forall x ((A \in C \land φ) \to z = A))$
44	43	imp	$⊢ (\forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \land \exists x (A \in C \land φ)) \to \exists z \in C \forall x ((A \in C \land φ) \to z = A)$
45		pm4.24	$⊢ (A \in C \land φ) \leftrightarrow ((A \in C \land φ) \land (A \in C \land φ))$
46	45	biimpi	$⊢ (A \in C \land φ) \to ((A \in C \land φ) \land (A \in C \land φ))$
47		anim12	$⊢ (((A \in C \land φ) \to z = A) \land ((A \in C \land φ) \to w = A)) \to (((A \in C \land φ) \land (A \in C \land φ)) \to (z = A \land w = A))$
48		eqtr3	$⊢ (z = A \land w = A) \to z = w$
49	46 47 48	syl56	$⊢ (((A \in C \land φ) \to z = A) \land ((A \in C \land φ) \to w = A)) \to ((A \in C \land φ) \to z = w)$
50	49	alanimi	$⊢ (\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to \forall x ((A \in C \land φ) \to z = w)$
51		19.23v	$⊢ \forall x ((A \in C \land φ) \to z = w) \leftrightarrow (\exists x (A \in C \land φ) \to z = w)$
52	50 51	sylib	$⊢ (\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to (\exists x (A \in C \land φ) \to z = w)$
53	52	com12	$⊢ \exists x (A \in C \land φ) \to ((\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to z = w)$
54	53	a1d	$⊢ \exists x (A \in C \land φ) \to ((z \in C \land w \in C) \to ((\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to z = w))$
55	54	ralrimivv	$⊢ \exists x (A \in C \land φ) \to \forall z \in C \forall w \in C ((\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to z = w)$
56	55	adantl	$⊢ (\forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \land \exists x (A \in C \land φ)) \to \forall z \in C \forall w \in C ((\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to z = w)$
57		eqeq1	$⊢ z = w \to (z = A \leftrightarrow w = A)$
58	57	imbi2d	$⊢ z = w \to (((A \in C \land φ) \to z = A) \leftrightarrow ((A \in C \land φ) \to w = A))$
59	58	albidv	$⊢ z = w \to (\forall x ((A \in C \land φ) \to z = A) \leftrightarrow \forall x ((A \in C \land φ) \to w = A))$
60	59	reu4	$⊢ \exists! z \in C \forall x ((A \in C \land φ) \to z = A) \leftrightarrow (\exists z \in C \forall x ((A \in C \land φ) \to z = A) \land \forall z \in C \forall w \in C ((\forall x ((A \in C \land φ) \to z = A) \land \forall x ((A \in C \land φ) \to w = A)) \to z = w))$
61	44 56 60	sylanbrc	$⊢ (\forall x \forall y (((A \in C \land φ) \land (B \in C \land ψ)) \to A = B) \land \exists x (A \in C \land φ)) \to \exists! z \in C \forall x ((A \in C \land φ) \to z = A)$

Metamath Proof Explorer

Theorem reuind

Proof