Metamath Proof Explorer


Theorem clel3

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

Ref Expression
Hypothesis clel3.1 𝐵 ∈ V
Assertion clel3 ( 𝐴𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵𝐴𝑥 ) )

Proof

Step Hyp Ref Expression
1 clel3.1 𝐵 ∈ V
2 clel3g ( 𝐵 ∈ V → ( 𝐴𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵𝐴𝑥 ) ) )
3 1 2 ax-mp ( 𝐴𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐵𝐴𝑥 ) )