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

Metamath Proof Explorer

Theorem reliin

Description: An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014)

Ref Expression
Assertion reliin ⊢ ∃ x ∈ A Rel ⁡ B → Rel ⁡ ⋂ x ∈ A B

Proof

Step Hyp Ref Expression
1 iinss ⊢ ∃ x ∈ A B ⊆ V × V → ⋂ x ∈ A B ⊆ V × V
2 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
3 2 rexbii ⊢ ∃ x ∈ A Rel ⁡ B ↔ ∃ x ∈ A B ⊆ V × V
4 df-rel ⊢ Rel ⁡ ⋂ x ∈ A B ↔ ⋂ x ∈ A B ⊆ V × V
5 1 3 4 3imtr4i ⊢ ∃ x ∈ A Rel ⁡ B → Rel ⁡ ⋂ x ∈ A B