Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Negated equality and membership
Negated equality
neqne
Next ⟩
neirr
Metamath Proof Explorer
Ascii
Structured
Theorem
neqne
Description:
From non-equality to inequality.
(Contributed by
Glauco Siliprandi
, 11-Dec-2019)
Ref
Expression
Assertion
neqne
⊢
( ¬
𝐴
=
𝐵
→
𝐴
≠
𝐵
)
Proof
Step
Hyp
Ref
Expression
1
id
⊢
( ¬
𝐴
=
𝐵
→ ¬
𝐴
=
𝐵
)
2
1
neqned
⊢
( ¬
𝐴
=
𝐵
→
𝐴
≠
𝐵
)