Definition df-op 4567

Description: Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)

Assertion

Ref	Expression
df-op	⊢ ⟨A, B⟩ = ({x ∣ ∃y ∈ A x = Phi y} ∪ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})

Distinct variable groups:   x,y,A   x,B,y

Detailed syntax breakdown of Definition df-op

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cop 4562	. 2 class ⟨A, B⟩
4		vx	. . . . . . 7 setvar x
5	4	cv 1641	. . . . . 6 class x
6		vy	. . . . . . . 8 setvar y
7	6	cv 1641	. . . . . . 7 class y
8	7	cphi 4563	. . . . . 6 class Phi y
9	5, 8	wceq 1642	. . . . 5 wff x = Phi y
10	9, 6, 1	wrex 2616	. . . 4 wff ∃y ∈ A x = Phi y
11	10, 4	cab 2339	. . 3 class {x ∣ ∃y ∈ A x = Phi y}
12		c0c 4375	. . . . . . . 8 class 0c
13	12	csn 3738	. . . . . . 7 class {0c}
14	8, 13	cun 3208	. . . . . 6 class ( Phi y ∪ {0c})
15	5, 14	wceq 1642	. . . . 5 wff x = ( Phi y ∪ {0c})
16	15, 6, 2	wrex 2616	. . . 4 wff ∃y ∈ B x = ( Phi y ∪ {0c})
17	16, 4	cab 2339	. . 3 class {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})}
18	11, 17	cun 3208	. 2 class ({x ∣ ∃y ∈ A x = Phi y} ∪ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})
19	3, 18	wceq 1642	1 wff ⟨A, B⟩ = ({x ∣ ∃y ∈ A x = Phi y} ∪ {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})})

This definition is referenced by:  dfop2  4576  proj1op  4601  proj2op  4602  nfop  4605  eqop  4612  opeq  4620  dfswap2  4742