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 ¬ ( 𝐴𝐵𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 elneq ( 𝐴𝐵𝐴𝐵 )
2 orc ( ¬ 𝐴𝐵 → ( ¬ 𝐴𝐵 ∨ ¬ 𝐴 = 𝐵 ) )
3 neneq ( 𝐴𝐵 → ¬ 𝐴 = 𝐵 )
4 3 olcd ( 𝐴𝐵 → ( ¬ 𝐴𝐵 ∨ ¬ 𝐴 = 𝐵 ) )
5 2 4 ja ( ( 𝐴𝐵𝐴𝐵 ) → ( ¬ 𝐴𝐵 ∨ ¬ 𝐴 = 𝐵 ) )
6 1 5 ax-mp ( ¬ 𝐴𝐵 ∨ ¬ 𝐴 = 𝐵 )
7 ianor ( ¬ ( 𝐴𝐵𝐴 = 𝐵 ) ↔ ( ¬ 𝐴𝐵 ∨ ¬ 𝐴 = 𝐵 ) )
8 6 7 mpbir ¬ ( 𝐴𝐵𝐴 = 𝐵 )