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

Metamath Proof Explorer

Theorem ineqri

Description: Inference from membership to intersection. (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Hypothesis	ineqri.1	$⊢ (x \in A \land x \in B) \leftrightarrow x \in C$
	Assertion	ineqri	$⊢ A \cap B = C$

Step	Hyp	Ref	Expression
1		ineqri.1	$⊢ (x \in A \land x \in B) \leftrightarrow x \in C$
2		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
3	2 1	bitri	$⊢ x \in (A \cap B) \leftrightarrow x \in C$
4	3	eqriv	$⊢ A \cap B = C$