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 )