Metamath Proof Explorer

Theorem rint0

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

Ref Expression
Assertion rint0 
|- ( X = (/) -> ( A i^i |^| X ) = A )

Proof

Step Hyp Ref Expression
1 inteq 
 |-  ( X = (/) -> |^| X = |^| (/) )
2 1 ineq2d 
 |-  ( X = (/) -> ( A i^i |^| X ) = ( A i^i |^| (/) ) )
3 int0 
 |-  |^| (/) = _V
4 3 ineq2i 
 |-  ( A i^i |^| (/) ) = ( A i^i _V )
5 inv1 
 |-  ( A i^i _V ) = A
6 4 5 eqtri 
 |-  ( A i^i |^| (/) ) = A
7 2 6 eqtrdi 
 |-  ( X = (/) -> ( A i^i |^| X ) = A )