Theorem uneq1

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	uneq1	|- ( A = B -> ( A u. C ) = ( B u. C ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( A = B -> ( x e. A <-> x e. B ) )
2	1	orbi1d	|- ( A = B -> ( ( x e. A \/ x e. C ) <-> ( x e. B \/ x e. C ) ) )
3		elun	|- ( x e. ( A u. C ) <-> ( x e. A \/ x e. C ) )
4		elun	|- ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5	2 3 4	3bitr4g	|- ( A = B -> ( x e. ( A u. C ) <-> x e. ( B u. C ) ) )
6	5	eqrdv	|- ( A = B -> ( A u. C ) = ( B u. C ) )