This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nelaneqOLD

Description: Obsolete version of nelaneq as of 31-Dec-2025. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nelaneqOLD ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵 )

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