Theorem clel3g

Description: An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005)

	Ref	Expression
Assertion	clel3g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
2	1	ceqsexgv	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥 ) ↔ 𝐴 ∈ 𝐵 ) )
3	2	bicomd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥 ) ) )