Theorem ineqri

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

	Ref	Expression
Hypothesis	ineqri.1	|- ( ( x e. A /\ x e. B ) <-> x e. C )
Assertion	ineqri	|- ( A i^i B ) = C

Proof

Step	Hyp	Ref	Expression
1		ineqri.1	|- ( ( x e. A /\ x e. B ) <-> x e. C )
2		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3	2 1	bitri	|- ( x e. ( A i^i B ) <-> x e. C )
4	3	eqriv	|- ( A i^i B ) = C