Definition df-si 4728

Description: Define the singleton image of a class. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-si	⊢ SI A = {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}

Distinct variable group:   x,A,y,z,w

Detailed syntax breakdown of Definition df-si

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csi 4720	. 2 class SI A
3		vx	. . . . . . . 8 setvar x
4	3	cv 1641	. . . . . . 7 class x
5		vz	. . . . . . . . 9 setvar z
6	5	cv 1641	. . . . . . . 8 class z
7	6	csn 3737	. . . . . . 7 class {z}
8	4, 7	wceq 1642	. . . . . 6 wff x = {z}
9		vy	. . . . . . . 8 setvar y
10	9	cv 1641	. . . . . . 7 class y
11		vw	. . . . . . . . 9 setvar w
12	11	cv 1641	. . . . . . . 8 class w
13	12	csn 3737	. . . . . . 7 class {w}
14	10, 13	wceq 1642	. . . . . 6 wff y = {w}
15	6, 12, 1	wbr 4639	. . . . . 6 wff zAw
16	8, 14, 15	w3a 934	. . . . 5 wff (x = {z} ∧ y = {w} ∧ zAw)
17	16, 11	wex 1541	. . . 4 wff ∃w(x = {z} ∧ y = {w} ∧ zAw)
18	17, 5	wex 1541	. . 3 wff ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)
19	18, 3, 9	copab 4622	. 2 class {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}
20	2, 19	wceq 1642	1 wff SI A = {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}

This definition is referenced by:  dfsi2  4751  brsi  4761  brsnsi  5773