df-opab

Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of Monk1 p. 34. Usually x and y are distinct, although the definition does not require it (see dfid2 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 . An example is given by ex-opab . (Contributed by NM, 4-Jul-1994)

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

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-opab

Detailed syntax breakdown