Theorem ssiin

Description: Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003)

	Ref	Expression
Assertion	ssiin	⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑥 𝐶
2	1	ssiinf	⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )