Metamath Proof Explorer


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 )