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