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

Metamath Proof Explorer

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 ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B

Proof

Step Hyp Ref Expression
1 iunss ⊢ ⋃ x ∈ A B ⊆ V × V ↔ ∀ x ∈ A B ⊆ V × V
2 df-rel ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ⋃ x ∈ A B ⊆ V × V
3 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
4 3 ralbii ⊢ ∀ x ∈ A Rel ⁡ B ↔ ∀ x ∈ A B ⊆ V × V
5 1 2 4 3bitr4i ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B