dfoprab2

Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995)

		Ref	Expression
	Assertion	dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$

Proof

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists z \exists w \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists w \exists z \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ))$
2		exrot4	$⊢ \exists z \exists w \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists x \exists y \exists z \exists w (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ))$
3		opeq1	$⊢ w = ⟨x, y⟩ \to ⟨w, z⟩ = ⟨⟨x, y⟩, z⟩$
4	3	eqeq2d	$⊢ w = ⟨x, y⟩ \to (v = ⟨w, z⟩ \leftrightarrow v = ⟨⟨x, y⟩, z⟩)$
5	4	pm5.32ri	$⊢ (v = ⟨w, z⟩ \land w = ⟨x, y⟩) \leftrightarrow (v = ⟨⟨x, y⟩, z⟩ \land w = ⟨x, y⟩)$
6	5	anbi1i	$⊢ ((v = ⟨w, z⟩ \land w = ⟨x, y⟩) \land φ) \leftrightarrow ((v = ⟨⟨x, y⟩, z⟩ \land w = ⟨x, y⟩) \land φ)$
7		anass	$⊢ ((v = ⟨w, z⟩ \land w = ⟨x, y⟩) \land φ) \leftrightarrow (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ))$
8		an32	$⊢ ((v = ⟨⟨x, y⟩, z⟩ \land w = ⟨x, y⟩) \land φ) \leftrightarrow ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land w = ⟨x, y⟩)$
9	6 7 8	3bitr3i	$⊢ (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land w = ⟨x, y⟩)$
10	9	exbii	$⊢ \exists w (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists w ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land w = ⟨x, y⟩)$
11		opex	$⊢ ⟨x, y⟩ \in V$
12	11	isseti	$⊢ \exists w w = ⟨x, y⟩$
13		19.42v	$⊢ \exists w ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land w = ⟨x, y⟩) \leftrightarrow ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land \exists w w = ⟨x, y⟩)$
14	12 13	mpbiran2	$⊢ \exists w ((v = ⟨⟨x, y⟩, z⟩ \land φ) \land w = ⟨x, y⟩) \leftrightarrow (v = ⟨⟨x, y⟩, z⟩ \land φ)$
15	10 14	bitri	$⊢ \exists w (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow (v = ⟨⟨x, y⟩, z⟩ \land φ)$
16	15	3exbii	$⊢ \exists x \exists y \exists z \exists w (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
17	2 16	bitri	$⊢ \exists z \exists w \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
18		19.42vv	$⊢ \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow (v = ⟨w, z⟩ \land \exists x \exists y (w = ⟨x, y⟩ \land φ))$
19	18	2exbii	$⊢ \exists w \exists z \exists x \exists y (v = ⟨w, z⟩ \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists w \exists z (v = ⟨w, z⟩ \land \exists x \exists y (w = ⟨x, y⟩ \land φ))$
20	1 17 19	3bitr3i	$⊢ \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists w \exists z (v = ⟨w, z⟩ \land \exists x \exists y (w = ⟨x, y⟩ \land φ))$
21	20	abbii	$⊢ \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\} = \{v \| \exists w \exists z (v = ⟨w, z⟩ \land \exists x \exists y (w = ⟨x, y⟩ \land φ))\}$
22		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
23		df-opab	$⊢ \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{v \| \exists w \exists z (v = ⟨w, z⟩ \land \exists x \exists y (w = ⟨x, y⟩ \land φ))\}$
24	21 22 23	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$

Metamath Proof Explorer

Theorem dfoprab2

Proof