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\exists yA=⟨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\leftrightarrow ⟨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\leftrightarrow \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\exists yA=⟨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$$