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

Metamath Proof Explorer

Theorem clel3g

Description: Alternate definition of membership in a set. (Contributed by NM, 13-Aug-2005)

Ref Expression
Assertion clel3g ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ x

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = B → A ∈ x ↔ A ∈ B
2 1 ceqsexgv ⊢ B ∈ V → ∃ x x = B ∧ A ∈ x ↔ A ∈ B
3 2 bicomd ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ x