Definition df-proj2 4569

Description: Define the second projection operation. This operation recovers the second element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)

Assertion

Ref	Expression
df-proj2	⊢ Proj2 A = {x ∣ ( Phi x ∪ {0c}) ∈ A}

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-proj2

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cproj2 4565	. 2 class Proj2 A
3		vx	. . . . . . 7 setvar x
4	3	cv 1641	. . . . . 6 class x
5	4	cphi 4563	. . . . 5 class Phi x
6		c0c 4375	. . . . . 6 class 0c
7	6	csn 3738	. . . . 5 class {0c}
8	5, 7	cun 3208	. . . 4 class ( Phi x ∪ {0c})
9	8, 1	wcel 1710	. . 3 wff ( Phi x ∪ {0c}) ∈ A
10	9, 3	cab 2339	. 2 class {x ∣ ( Phi x ∪ {0c}) ∈ A}
11	2, 10	wceq 1642	1 wff Proj2 A = {x ∣ ( Phi x ∪ {0c}) ∈ A}

This definition is referenced by:  dfproj22  4578  proj2op  4602  opeq  4620