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

Metamath Proof Explorer

Theorem elimel

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case B e. C is provable. (Contributed by NM, 15-May-1999)

		Ref	Expression
	Hypothesis	elimel.1	$⊢ B \in C$
	Assertion	elimel	$⊢ if (A \in C, A, B) \in C$

Step	Hyp	Ref	Expression
1		elimel.1	$⊢ B \in C$
2		eleq1	$⊢ A = if (A \in C, A, B) \to (A \in C \leftrightarrow if (A \in C, A, B) \in C)$
3		eleq1	$⊢ B = if (A \in C, A, B) \to (B \in C \leftrightarrow if (A \in C, A, B) \in C)$
4	2 3 1	elimhyp	$⊢ if (A \in C, A, B) \in C$