This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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