Theorem riinn0

Description: Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	riinn0	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 )
2		r19.2z	⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
3	2	ancoms	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
4		iinss	⊢ ( ∃ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
5	3 4	syl	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 )
6		df-ss	⊢ ( ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ↔ ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )
7	5 6	sylib	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( ∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )
8	1 7	syl5eq	⊢ ( ( ∀ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ∩ 𝑥 ∈ 𝑋 𝑆 )