Metamath Proof Explorer

Theorem disjresin

Description: The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion disjresin 
|- ( ( A i^i B ) = (/) -> ( R |` ( A i^i B ) ) = (/) )

Proof

Step Hyp Ref Expression
1 reseq2 
 |-  ( ( A i^i B ) = (/) -> ( R |` ( A i^i B ) ) = ( R |` (/) ) )
2 res0 
 |-  ( R |` (/) ) = (/)
3 1 2 eqtrdi 
 |-  ( ( A i^i B ) = (/) -> ( R |` ( A i^i B ) ) = (/) )