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 ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
2	1	releqi	⊢ ( Rel ∪ 𝐴 ↔ Rel ∪ 𝑥 ∈ 𝐴 𝑥 )
3		reliun	⊢ ( Rel ∪ 𝑥 ∈ 𝐴 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝑥 )
4	2 3	bitri	⊢ ( Rel ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝑥 )