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	|- ( Rel U_ x e. A B <-> A. x e. A Rel B )

Proof

Step	Hyp	Ref	Expression
1		iunss	|- ( U_ x e. A B C_ ( _V X. _V ) <-> A. x e. A B C_ ( _V X. _V ) )
2		df-rel	|- ( Rel U_ x e. A B <-> U_ x e. A B C_ ( _V X. _V ) )
3		df-rel	|- ( Rel B <-> B C_ ( _V X. _V ) )
4	3	ralbii	|- ( A. x e. A Rel B <-> A. x e. A B C_ ( _V X. _V ) )
5	1 2 4	3bitr4i	|- ( Rel U_ x e. A B <-> A. x e. A Rel B )