Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Negated equality and membership
Negated equality
necon1bd
Metamath Proof Explorer
Description: Contrapositive deduction for inequality. (Contributed by NM , 21-Mar-2007) (Proof shortened by Andrew Salmon , 25-May-2011) (Proof
shortened by Wolf Lammen , 23-Nov-2019)

Ref
Expression
Hypothesis
necon1bd.1
$${\u22a2}{\phi}\to \left({A}\ne {B}\to {\psi}\right)$$
Assertion
necon1bd
$${\u22a2}{\phi}\to \left(\neg {\psi}\to {A}={B}\right)$$

Proof
Step
Hyp
Ref
Expression
1
necon1bd.1
$${\u22a2}{\phi}\to \left({A}\ne {B}\to {\psi}\right)$$
2
df-ne
$${\u22a2}{A}\ne {B}\leftrightarrow \neg {A}={B}$$
3
2 1
syl5bir
$${\u22a2}{\phi}\to \left(\neg {A}={B}\to {\psi}\right)$$
4
3
con1d
$${\u22a2}{\phi}\to \left(\neg {\psi}\to {A}={B}\right)$$