New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nne | GIF version |
Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.) |
Ref | Expression |
---|---|
nne | ⊢ (¬ A ≠ B ↔ A = B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2518 | . . 3 ⊢ (A ≠ B ↔ ¬ A = B) | |
2 | 1 | con2bii 322 | . 2 ⊢ (A = B ↔ ¬ A ≠ B) |
3 | 2 | bicomi 193 | 1 ⊢ (¬ A ≠ B ↔ A = B) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 176 = wceq 1642 ≠ wne 2516 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-ne 2518 |
This theorem is referenced by: neirr 2521 necon3ad 2552 necon3bd 2553 necon3ai 2556 necon3bi 2557 necon1bi 2559 necon2ai 2561 necon2ad 2564 necon4ai 2575 necon4i 2576 necon4ad 2577 necon4bd 2578 necon4d 2579 necon4bid 2582 necon1bd 2584 necon1d 2585 pm2.61ne 2591 pm2.61ine 2592 pm2.61dne 2593 ne3anior 2602 sbcne12g 3154 xpeq0 5046 xpcan 5057 xpcan2 5058 |
Copyright terms: Public domain | W3C validator |