Metamath Proof Explorer


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 ( 𝑋 = ∅ → ( 𝐴 𝑋 ) = 𝐴 )