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 RelRARAR

Proof

Step Hyp Ref Expression
1 elrel RelRARxyA=xy
2 simpr RelRARAR
3 vex xV
4 vex yV
5 3 4 uniopel xyRxyR
6 5 a1i A=xyxyRxyR
7 eleq1 A=xyARxyR
8 unieq A=xyA=xy
9 8 eleq1d A=xyARxyR
10 6 7 9 3imtr4d A=xyARAR
11 10 exlimivv xyA=xyARAR
12 1 2 11 sylc RelRARAR