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
|- ( A e. B -/\ B e. A )

Proof

Step Hyp Ref Expression
1 en2lp
 |-  -. ( A e. B /\ B e. A )
2 df-nan
 |-  ( ( A e. B -/\ B e. A ) <-> -. ( A e. B /\ B e. A ) )
3 1 2 mpbir
 |-  ( A e. B -/\ B e. A )