Metamath Proof Explorer

Theorem bj-elsnb

Description: Biconditional version of elsng . (Contributed by BJ, 18-Nov-2023)

Ref Expression
Assertion bj-elsnb 
|- ( A e. { B } <-> ( A e. _V /\ A = B ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. { B } -> A e. _V )
2 elsng 
 |-  ( A e. _V -> ( A e. { B } <-> A = B ) )
3 1 2 biadanii 
 |-  ( A e. { B } <-> ( A e. _V /\ A = B ) )