HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-eprel 2821
Description: Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
Assertion
Ref Expression
df-eprel |- E = {<.x, y>. | x e. y}
Distinct variable group:   x,y
Detailed syntax breakdown of Definition df-eprel
StepHypRef Expression
1 cep 2819 . 2 class E
2 vx . . . . 5 set x
32cv 952 . . . 4 class x
4 vy . . . . 5 set y
54cv 952 . . . 4 class y
63, 5wcel 955 . . 3 wff x e. y
76, 2, 4copab 2656 . 2 class {<.x, y>. | x e. y}
81, 7wceq 953 1 wff E = {<.x, y>. | x e. y}
Colors of variables: wff set class
This definition is referenced by:  epelc 2822  rele 3264
Copyright terms: Public domain