Theorem uneqri

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

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

Proof

Step	Hyp	Ref	Expression
1		uneqri.1	|- ( ( x e. A \/ x e. B ) <-> x e. C )
2		elun	|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
3	2 1	bitri	|- ( x e. ( A u. B ) <-> x e. C )
4	3	eqriv	|- ( A u. B ) = C