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