# 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 )`