Metamath Proof Explorer


Theorem clel2

Description: Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis clel2.1 𝐴 ∈ V
Assertion clel2 ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 clel2.1 𝐴 ∈ V
2 clel2g ( 𝐴 ∈ V → ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) ) )
3 1 2 ax-mp ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) )