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

Metamath Proof Explorer

Theorem iinssf

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis iinssf.1 ⊢ Ⅎ 𝑥 𝐶
Assertion iinssf ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 iinssf.1 ⊢ Ⅎ 𝑥 𝐶
2 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
3 2 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
4 ssel ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
5 4 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
6 1 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
7 6 r19.36vf ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
8 5 7 syl ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
9 3 8 biimtrid ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶 ) )
10 9 ssrdv ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )