Metamath Proof Explorer


Definition df-eprel

Description: Define the membership relation (also called "epsilon relation" since it is sometimes denoted by the lowercase Greek letter "epsilon"). Similar to Definition 6.22 of TakeutiZaring p. 30. The membership relation and the membership predicate agree, that is, ( AE B <-> A e. B ) , when B is a set (see epelg ). Thus, |- 5 E { 1 , 5 } ( ex-eprel ). (Contributed by NM, 13-Aug-1995)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cep
 |-  _E
1 vx
 |-  x
2 vy
 |-  y
3 1 cv
 |-  x
4 2 cv
 |-  y
5 3 4 wcel
 |-  x e. y
6 5 1 2 copab
 |-  { <. x , y >. | x e. y }
7 0 6 wceq
 |-  _E = { <. x , y >. | x e. y }