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

Metamath Proof Explorer

Theorem ssiinf

Description: Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012) (Proof shortened by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypothesis ssiinf.1 ⊢ Ⅎ 𝑥 𝐶
Assertion ssiinf ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 ssiinf.1 ⊢ Ⅎ 𝑥 𝐶
2 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
3 2 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
4 3 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐶 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5 nfcv ⊢ Ⅎ 𝑦 𝐴
6 1 5 ralcomf ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑦 ∈ 𝐵 )
7 4 6 bitri ⊢ ( ∀ 𝑦 ∈ 𝐶 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑦 ∈ 𝐵 )
8 dfss3 ⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐶 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 )
9 dfss3 ⊢ ( 𝐶 ⊆ 𝐵 ↔ ∀ 𝑦 ∈ 𝐶 𝑦 ∈ 𝐵 )
10 9 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑦 ∈ 𝐵 )
11 7 8 10 3bitr4i ⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )