Theorem rintn0

Description: Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Assertion	rintn0	⊢ ( ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑋 ) = ∩ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		intssuni2	⊢ ( ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) → ∩ 𝑋 ⊆ ∪ 𝒫 𝐴 )
2		ssid	⊢ 𝒫 𝐴 ⊆ 𝒫 𝐴
3		sspwuni	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐴 ↔ ∪ 𝒫 𝐴 ⊆ 𝐴 )
4	2 3	mpbi	⊢ ∪ 𝒫 𝐴 ⊆ 𝐴
5	1 4	sstrdi	⊢ ( ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) → ∩ 𝑋 ⊆ 𝐴 )
6		sseqin2	⊢ ( ∩ 𝑋 ⊆ 𝐴 ↔ ( 𝐴 ∩ ∩ 𝑋 ) = ∩ 𝑋 )
7	5 6	sylib	⊢ ( ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑋 ) = ∩ 𝑋 )