Definition df-eprel 5553

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, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵), when 𝐵 is a set (see epelg 5554). Thus, ⊢ 5 E {1, 5} (ex-eprel 30360). (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
df-eprel	⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-eprel

Step	Hyp	Ref	Expression
1		cep 5552	. 2 class E
2		vx	. . . 4 setvar 𝑥
3		vy	. . . 4 setvar 𝑦
4	2, 3	wel 2109	. . 3 wff 𝑥 ∈ 𝑦
5	4, 2, 3	copab 5181	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	1, 5	wceq 1540	1 wff E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

This definition is referenced by:  epelg  5554  rele  5806  epinid0  9612  cnvepnep  9620  bj-epelg  37032  dfnelbr2  47250