# 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 ${⊢}\left(\mathrm{Rel}{R}\wedge {A}\in {R}\right)\to \bigcup {A}\in \bigcup {R}$

### Proof

Step Hyp Ref Expression
1 elrel ${⊢}\left(\mathrm{Rel}{R}\wedge {A}\in {R}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{A}=⟨{x},{y}⟩$
2 simpr ${⊢}\left(\mathrm{Rel}{R}\wedge {A}\in {R}\right)\to {A}\in {R}$
3 vex ${⊢}{x}\in \mathrm{V}$
4 vex ${⊢}{y}\in \mathrm{V}$
5 3 4 uniopel ${⊢}⟨{x},{y}⟩\in {R}\to \bigcup ⟨{x},{y}⟩\in \bigcup {R}$
6 5 a1i ${⊢}{A}=⟨{x},{y}⟩\to \left(⟨{x},{y}⟩\in {R}\to \bigcup ⟨{x},{y}⟩\in \bigcup {R}\right)$
7 eleq1 ${⊢}{A}=⟨{x},{y}⟩\to \left({A}\in {R}↔⟨{x},{y}⟩\in {R}\right)$
8 unieq ${⊢}{A}=⟨{x},{y}⟩\to \bigcup {A}=\bigcup ⟨{x},{y}⟩$
9 8 eleq1d ${⊢}{A}=⟨{x},{y}⟩\to \left(\bigcup {A}\in \bigcup {R}↔\bigcup ⟨{x},{y}⟩\in \bigcup {R}\right)$
10 6 7 9 3imtr4d ${⊢}{A}=⟨{x},{y}⟩\to \left({A}\in {R}\to \bigcup {A}\in \bigcup {R}\right)$
11 10 exlimivv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{A}=⟨{x},{y}⟩\to \left({A}\in {R}\to \bigcup {A}\in \bigcup {R}\right)$
12 1 2 11 sylc ${⊢}\left(\mathrm{Rel}{R}\wedge {A}\in {R}\right)\to \bigcup {A}\in \bigcup {R}$