Definition df-eprel 5465

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 5466). Thus, ⊢ 5 E {1, 5} (ex-eprel 28212). (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 5464	. 2 class E
2		vx	. . . 4 setvar 𝑥
3		vy	. . . 4 setvar 𝑦
4	2, 3	wel 2115	. . 3 wff 𝑥 ∈ 𝑦
5	4, 2, 3	copab 5128	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	1, 5	wceq 1537	1 wff E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

This definition is referenced by:  epelg  5466  epelgOLD  5467  rele  5699  epinid0  9064  cnvepnep  9071  bj-epelg  34363  dfnelbr2  43521