Metamath Proof Explorer


Theorem clel3g

Description: Alternate definition of membership in 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 ( 𝐵𝑉 → ( 𝐴𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵𝐴𝑥 ) ) )