Definition df-eprel 4267

Description: Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, ( A _E B <-> A e. B ) when B is a set by epelg 4268. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
df-eprel	|- _E = { <. x , y >. | x e. y }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-eprel

Step	Hyp	Ref	Expression
1		cep 4265	. 2 class _E
2		vx	. . . 4 setvar x
3		vy	. . . 4 setvar y
4	2, 3	wel 2137	. . 3 wff x e. y
5	4, 2, 3	copab 4042	. 2 class { <. x , y >. | x e. y }
6	1, 5	wceq 1343	1 wff _E = { <. x , y >. | x e. y }

This definition is referenced by:  epelg  4268  rele  4734