Definition df-eprel 5029

Description: Define the membership relation, or 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 5030. Thus, 5 _E { 1 , 5 } (ex-eprel 27290). (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 5028	. 2 class _E
2		vx	. . . 4 setvar x
3		vy	. . . 4 setvar y
4	2, 3	wel 1991	. . 3 wff x e. y
5	4, 2, 3	copab 4712	. 2 class { <. x , y >. | x e. y }
6	1, 5	wceq 1483	1 wff _E = { <. x , y >. | x e. y }

This definition is referenced by:  epelg  5030  rele  5250  dfnelbr2  41290