This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjresundif

Description: Lemma for ressucdifsn2 . (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion disjresundif 
|- ( ( A i^i B ) = (/) -> ( ( R |` ( A u. B ) ) \ ( R |` B ) ) = ( R |` A ) )

Proof

Step Hyp Ref Expression
1 resundi 
 |-  ( R |` ( A u. B ) ) = ( ( R |` A ) u. ( R |` B ) )
2 1 difeq1i 
 |-  ( ( R |` ( A u. B ) ) \ ( R |` B ) ) = ( ( ( R |` A ) u. ( R |` B ) ) \ ( R |` B ) )
3 difun2 
 |-  ( ( ( R |` A ) u. ( R |` B ) ) \ ( R |` B ) ) = ( ( R |` A ) \ ( R |` B ) )
4 2 3 eqtri 
 |-  ( ( R |` ( A u. B ) ) \ ( R |` B ) ) = ( ( R |` A ) \ ( R |` B ) )
5 disjresdif 
 |-  ( ( A i^i B ) = (/) -> ( ( R |` A ) \ ( R |` B ) ) = ( R |` A ) )
6 4 5 eqtrid 
 |-  ( ( A i^i B ) = (/) -> ( ( R |` ( A u. B ) ) \ ( R |` B ) ) = ( R |` A ) )