Theorem reluni

Description: The union of a class is a relation iff any member is a relation. Exercise 6 of TakeutiZaring p. 25 and its converse. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	reluni	|- ( Rel U. A <-> A. x e. A Rel x )

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. A = U_ x e. A x
2	1	releqi	|- ( Rel U. A <-> Rel U_ x e. A x )
3		reliun	|- ( Rel U_ x e. A x <-> A. x e. A Rel x )
4	2 3	bitri	|- ( Rel U. A <-> A. x e. A Rel x )