Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Negated equality and membership
Negated equality
necomi
Next ⟩
necomd
Metamath Proof Explorer
Ascii
Unicode
Theorem
necomi
Description:
Inference from commutative law for inequality.
(Contributed by
NM
, 17-Oct-2012)
Ref
Expression
Hypothesis
necomi.1
⊢
A
≠
B
Assertion
necomi
⊢
B
≠
A
Proof
Step
Hyp
Ref
Expression
1
necomi.1
⊢
A
≠
B
2
necom
⊢
A
≠
B
↔
B
≠
A
3
1
2
mpbi
⊢
B
≠
A