This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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