Metamath Proof Explorer


Theorem elnanel

Description: Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp and serves as an example in the context of Godel codes, see elnanelprv . (Contributed by AV, 5-Nov-2023) (New usage is discouraged.)

Ref Expression
Assertion elnanel ( 𝐴𝐵𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 en2lp ¬ ( 𝐴𝐵𝐵𝐴 )
2 df-nan ( ( 𝐴𝐵𝐵𝐴 ) ↔ ¬ ( 𝐴𝐵𝐵𝐴 ) )
3 1 2 mpbir ( 𝐴𝐵𝐵𝐴 )