Theorem riin0

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

	Ref	Expression
Assertion	riin0	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iineq1	⊢ ( 𝑋 = ∅ → ∩ 𝑥 ∈ 𝑋 𝑆 = ∩ 𝑥 ∈ ∅ 𝑆 )
2	1	ineq2d	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = ( 𝐴 ∩ ∩ 𝑥 ∈ ∅ 𝑆 ) )
3		0iin	⊢ ∩ 𝑥 ∈ ∅ 𝑆 = V
4	3	ineq2i	⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ ∅ 𝑆 ) = ( 𝐴 ∩ V )
5		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
6	4 5	eqtri	⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ ∅ 𝑆 ) = 𝐴
7	2 6	syl6eq	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) = 𝐴 )