Definition df-eprel 5445

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 5446). Thus, ⊢ 5 E {1, 5} (ex-eprel 28470). (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 5444	. 2 class E
2		vx	. . . 4 setvar 𝑥
3		vy	. . . 4 setvar 𝑦
4	2, 3	wel 2113	. . 3 wff 𝑥 ∈ 𝑦
5	4, 2, 3	copab 5101	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	1, 5	wceq 1543	1 wff E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

This definition is referenced by:  epelg  5446  rele  5682  epinid0  9194  cnvepnep  9201  bj-epelg  34924  dfnelbr2  44380