dfac5lem1

		Ref	Expression
	Assertion	dfac5lem1	$⊢ \exists! v v \in ((\{w\} \times w) \cap y) \leftrightarrow \exists! g (g \in w \land ⟨w, g⟩ \in y)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ v \in ((\{w\} \times w) \cap y) \leftrightarrow (v \in (\{w\} \times w) \land v \in y)$
2		elxp	$⊢ v \in (\{w\} \times w) \leftrightarrow \exists t \exists g (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w))$
3		excom	$⊢ \exists t \exists g (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \leftrightarrow \exists g \exists t (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w))$
4	2 3	bitri	$⊢ v \in (\{w\} \times w) \leftrightarrow \exists g \exists t (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w))$
5	4	anbi1i	$⊢ (v \in (\{w\} \times w) \land v \in y) \leftrightarrow (\exists g \exists t (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y)$
6		19.41vv	$⊢ \exists g \exists t ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow (\exists g \exists t (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y)$
7		an32	$⊢ ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow ((v = ⟨t, g⟩ \land v \in y) \land (t \in \{w\} \land g \in w))$
8		eleq1	$⊢ v = ⟨t, g⟩ \to (v \in y \leftrightarrow ⟨t, g⟩ \in y)$
9	8	pm5.32i	$⊢ (v = ⟨t, g⟩ \land v \in y) \leftrightarrow (v = ⟨t, g⟩ \land ⟨t, g⟩ \in y)$
10		velsn	$⊢ t \in \{w\} \leftrightarrow t = w$
11	10	anbi1i	$⊢ (t \in \{w\} \land g \in w) \leftrightarrow (t = w \land g \in w)$
12	9 11	anbi12i	$⊢ ((v = ⟨t, g⟩ \land v \in y) \land (t \in \{w\} \land g \in w)) \leftrightarrow ((v = ⟨t, g⟩ \land ⟨t, g⟩ \in y) \land (t = w \land g \in w))$
13		an4	$⊢ ((v = ⟨t, g⟩ \land ⟨t, g⟩ \in y) \land (t = w \land g \in w)) \leftrightarrow ((v = ⟨t, g⟩ \land t = w) \land (⟨t, g⟩ \in y \land g \in w))$
14		ancom	$⊢ (v = ⟨t, g⟩ \land t = w) \leftrightarrow (t = w \land v = ⟨t, g⟩)$
15		ancom	$⊢ (⟨t, g⟩ \in y \land g \in w) \leftrightarrow (g \in w \land ⟨t, g⟩ \in y)$
16	14 15	anbi12i	$⊢ ((v = ⟨t, g⟩ \land t = w) \land (⟨t, g⟩ \in y \land g \in w)) \leftrightarrow ((t = w \land v = ⟨t, g⟩) \land (g \in w \land ⟨t, g⟩ \in y))$
17		anass	$⊢ ((t = w \land v = ⟨t, g⟩) \land (g \in w \land ⟨t, g⟩ \in y)) \leftrightarrow (t = w \land (v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y)))$
18	13 16 17	3bitri	$⊢ ((v = ⟨t, g⟩ \land ⟨t, g⟩ \in y) \land (t = w \land g \in w)) \leftrightarrow (t = w \land (v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y)))$
19	7 12 18	3bitri	$⊢ ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow (t = w \land (v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y)))$
20	19	exbii	$⊢ \exists t ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow \exists t (t = w \land (v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y)))$
21		opeq1	$⊢ t = w \to ⟨t, g⟩ = ⟨w, g⟩$
22	21	eqeq2d	$⊢ t = w \to (v = ⟨t, g⟩ \leftrightarrow v = ⟨w, g⟩)$
23	21	eleq1d	$⊢ t = w \to (⟨t, g⟩ \in y \leftrightarrow ⟨w, g⟩ \in y)$
24	23	anbi2d	$⊢ t = w \to ((g \in w \land ⟨t, g⟩ \in y) \leftrightarrow (g \in w \land ⟨w, g⟩ \in y))$
25	22 24	anbi12d	$⊢ t = w \to ((v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y)) \leftrightarrow (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y)))$
26	25	equsexvw	$⊢ \exists t (t = w \land (v = ⟨t, g⟩ \land (g \in w \land ⟨t, g⟩ \in y))) \leftrightarrow (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
27	20 26	bitri	$⊢ \exists t ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
28	27	exbii	$⊢ \exists g \exists t ((v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow \exists g (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
29	6 28	bitr3i	$⊢ (\exists g \exists t (v = ⟨t, g⟩ \land (t \in \{w\} \land g \in w)) \land v \in y) \leftrightarrow \exists g (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
30	1 5 29	3bitri	$⊢ v \in ((\{w\} \times w) \cap y) \leftrightarrow \exists g (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
31	30	eubii	$⊢ \exists! v v \in ((\{w\} \times w) \cap y) \leftrightarrow \exists! v \exists g (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y))$
32		vex	$⊢ w \in V$
33	32	euop2	$⊢ \exists! v \exists g (v = ⟨w, g⟩ \land (g \in w \land ⟨w, g⟩ \in y)) \leftrightarrow \exists! g (g \in w \land ⟨w, g⟩ \in y)$
34	31 33	bitri	$⊢ \exists! v v \in ((\{w\} \times w) \cap y) \leftrightarrow \exists! g (g \in w \land ⟨w, g⟩ \in y)$

Metamath Proof Explorer

Theorem dfac5lem1

Proof