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	⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )