df-oprab

Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of TakeutiZaring p. 14. Normally x , y , and z are distinct, although the definition doesn't strictly require it. See df-ov for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of an operation given by a class abstraction is given by ovmpo . (Contributed by NM, 12-Mar-1995)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		vy	$setvar y$
2		vz	$setvar z$
3		wph	$wff φ$
4	3 0 1 2	coprab	$class \{⟨⟨x, y⟩, z⟩ \| φ\}$
5		vw	$setvar w$
6	5	cv	$setvar w$
7	0	cv	$setvar x$
8	1	cv	$setvar y$
9	7 8	cop	$class ⟨x, y⟩$
10	2	cv	$setvar z$
11	9 10	cop	$class ⟨⟨x, y⟩, z⟩$
12	6 11	wceq	$wff w = ⟨⟨x, y⟩, z⟩$
13	12 3	wa	$wff (w = ⟨⟨x, y⟩, z⟩ \land φ)$
14	13 2	wex	$wff \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
15	14 1	wex	$wff \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
16	15 0	wex	$wff \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
17	16 5	cab	$class \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
18	4 17	wceq	$wff \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$

Metamath Proof Explorer

Definition df-oprab

Detailed syntax breakdown