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

Metamath Proof Explorer

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 )