Metamath Proof Explorer


Theorem nnel

Description: Negation of negated membership, analogous to nne . (Contributed by Alexander van der Vekens, 18-Jan-2018) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Assertion nnel ( ¬ 𝐴𝐵𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 df-nel ( 𝐴𝐵 ↔ ¬ 𝐴𝐵 )
2 1 bicomi ( ¬ 𝐴𝐵𝐴𝐵 )
3 2 con1bii ( ¬ 𝐴𝐵𝐴𝐵 )