Theorem unielrel

Description: The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	unielrel	|- ( ( Rel R /\ A e. R ) -> U. A e. U. R )

Proof

Step	Hyp	Ref	Expression
1		elrel	|- ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )
2		simpr	|- ( ( Rel R /\ A e. R ) -> A e. R )
3		vex	|- x e. _V
4		vex	|- y e. _V
5	3 4	uniopel	|- ( <. x , y >. e. R -> U. <. x , y >. e. U. R )
6	5	a1i	|- ( A = <. x , y >. -> ( <. x , y >. e. R -> U. <. x , y >. e. U. R ) )
7		eleq1	|- ( A = <. x , y >. -> ( A e. R <-> <. x , y >. e. R ) )
8		unieq	|- ( A = <. x , y >. -> U. A = U. <. x , y >. )
9	8	eleq1d	|- ( A = <. x , y >. -> ( U. A e. U. R <-> U. <. x , y >. e. U. R ) )
10	6 7 9	3imtr4d	|- ( A = <. x , y >. -> ( A e. R -> U. A e. U. R ) )
11	10	exlimivv	|- ( E. x E. y A = <. x , y >. -> ( A e. R -> U. A e. U. R ) )
12	1 2 11	sylc	|- ( ( Rel R /\ A e. R ) -> U. A e. U. R )