Theorem reliun

Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008) (Proof shortened by SN, 2-Feb-2025)

	Ref	Expression
Assertion	reliun	$$⊢\mathrm{Rel}\bigcup _{x\in A}B\leftrightarrow \forall x\in A\mathrm{Rel}B$$

Proof

Step	Hyp	Ref	Expression
1		iunss	$$⊢\bigcup _{x\in A}B\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow \forall x\in AB\subseteq \mathrm{V}\times \mathrm{V}$$
2		df-rel	$$⊢\mathrm{Rel}\bigcup _{x\in A}B\leftrightarrow \bigcup _{x\in A}B\subseteq \mathrm{V}\times \mathrm{V}$$
3		df-rel	$$⊢\mathrm{Rel}B\leftrightarrow B\subseteq \mathrm{V}\times \mathrm{V}$$
4	3	ralbii	$$⊢\forall x\in A\mathrm{Rel}B\leftrightarrow \forall x\in AB\subseteq \mathrm{V}\times \mathrm{V}$$
5	1 2 4	3bitr4i	$$⊢\mathrm{Rel}\bigcup _{x\in A}B\leftrightarrow \forall x\in A\mathrm{Rel}B$$