This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neleq12d

Description: Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Hypotheses	neleq12d.1	$⊢ φ \to A = B$
	neleq12d.2	$⊢ φ \to C = D$
Assertion	neleq12d	$⊢ φ \to (A \notin C \leftrightarrow B \notin D)$

Step	Hyp	Ref	Expression
1		neleq12d.1	$⊢ φ \to A = B$
2		neleq12d.2	$⊢ φ \to C = D$
3	1 2	eleq12d	$⊢ φ \to (A \in C \leftrightarrow B \in D)$
4	3	notbid	$⊢ φ \to (\neg A \in C \leftrightarrow \neg B \in D)$
5		df-nel	$⊢ A \notin C \leftrightarrow \neg A \in C$
6		df-nel	$⊢ B \notin D \leftrightarrow \neg B \in D$
7	4 5 6	3bitr4g	$⊢ φ \to (A \notin C \leftrightarrow B \notin D)$