Metamath Proof Explorer


Theorem nelaneq

Description: A class is not an element of and equal to a class at the same time. Variant of elneq analogously to elnotel and en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022)

Ref Expression
Assertion nelaneq
|- -. ( A e. B /\ A = B )

Proof

Step Hyp Ref Expression
1 elneq
 |-  ( A e. B -> A =/= B )
2 orc
 |-  ( -. A e. B -> ( -. A e. B \/ -. A = B ) )
3 neneq
 |-  ( A =/= B -> -. A = B )
4 3 olcd
 |-  ( A =/= B -> ( -. A e. B \/ -. A = B ) )
5 2 4 ja
 |-  ( ( A e. B -> A =/= B ) -> ( -. A e. B \/ -. A = B ) )
6 1 5 ax-mp
 |-  ( -. A e. B \/ -. A = B )
7 ianor
 |-  ( -. ( A e. B /\ A = B ) <-> ( -. A e. B \/ -. A = B ) )
8 6 7 mpbir
 |-  -. ( A e. B /\ A = B )