Theorem dfclel

Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	dfclel	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cleljust	⊢ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑢 ( 𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧 ) )
2		cleljust	⊢ ( 𝑡 ∈ 𝑡 ↔ ∃ 𝑣 ( 𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡 ) )
3	1 2	df-clel	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )