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 ( ∃ 𝑥𝐴 Rel 𝐵 → Rel 𝑥𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 iinss ( ∃ 𝑥𝐴 𝐵 ⊆ ( V × V ) → 𝑥𝐴 𝐵 ⊆ ( V × V ) )
2 df-rel ( Rel 𝐵𝐵 ⊆ ( V × V ) )
3 2 rexbii ( ∃ 𝑥𝐴 Rel 𝐵 ↔ ∃ 𝑥𝐴 𝐵 ⊆ ( V × V ) )
4 df-rel ( Rel 𝑥𝐴 𝐵 𝑥𝐴 𝐵 ⊆ ( V × V ) )
5 1 3 4 3imtr4i ( ∃ 𝑥𝐴 Rel 𝐵 → Rel 𝑥𝐴 𝐵 )