Theorem rint0

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

	Ref	Expression
Assertion	rint0	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑋 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		inteq	⊢ ( 𝑋 = ∅ → ∩ 𝑋 = ∩ ∅ )
2	1	ineq2d	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑋 ) = ( 𝐴 ∩ ∩ ∅ ) )
3		int0	⊢ ∩ ∅ = V
4	3	ineq2i	⊢ ( 𝐴 ∩ ∩ ∅ ) = ( 𝐴 ∩ V )
5		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
6	4 5	eqtri	⊢ ( 𝐴 ∩ ∩ ∅ ) = 𝐴
7	2 6	eqtrdi	⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑋 ) = 𝐴 )