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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cep	⊢ E
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	2	cv	⊢ 𝑦
5	3 4	wcel	⊢ 𝑥 ∈ 𝑦
6	5 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }
7	0 6	wceq	⊢ E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }