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

Metamath Proof Explorer

Theorem psdmullem

Description: Lemma for psdmul . Transitive law for union of class difference. (Contributed by SN, 5-May-2025)

Ref Expression
Hypotheses psdmullem.cb 
|- ( ph -> C C_ B )
psdmullem.ba 
|- ( ph -> B C_ A )
Assertion psdmullem 
|- ( ph -> ( ( A \ B ) u. ( B \ C ) ) = ( A \ C ) )

Proof

Step Hyp Ref Expression
1 psdmullem.cb 
 |-  ( ph -> C C_ B )
2 psdmullem.ba 
 |-  ( ph -> B C_ A )
3 undif3 
 |-  ( ( A \ B ) u. ( B \ C ) ) = ( ( ( A \ B ) u. B ) \ ( C \ ( A \ B ) ) )
4 undifr 
 |-  ( B C_ A <-> ( ( A \ B ) u. B ) = A )
5 2 4 sylib 
 |-  ( ph -> ( ( A \ B ) u. B ) = A )
6 difdif2 
 |-  ( C \ ( A \ B ) ) = ( ( C \ A ) u. ( C i^i B ) )
7 1 2 sstrd 
 |-  ( ph -> C C_ A )
8 ssdif0 
 |-  ( C C_ A <-> ( C \ A ) = (/) )
9 7 8 sylib 
 |-  ( ph -> ( C \ A ) = (/) )
10 dfss2 
 |-  ( C C_ B <-> ( C i^i B ) = C )
11 1 10 sylib 
 |-  ( ph -> ( C i^i B ) = C )
12 9 11 uneq12d 
 |-  ( ph -> ( ( C \ A ) u. ( C i^i B ) ) = ( (/) u. C ) )
13 0un 
 |-  ( (/) u. C ) = C
14 12 13 eqtrdi 
 |-  ( ph -> ( ( C \ A ) u. ( C i^i B ) ) = C )
15 6 14 eqtrid 
 |-  ( ph -> ( C \ ( A \ B ) ) = C )
16 5 15 difeq12d 
 |-  ( ph -> ( ( ( A \ B ) u. B ) \ ( C \ ( A \ B ) ) ) = ( A \ C ) )
17 3 16 eqtrid 
 |-  ( ph -> ( ( A \ B ) u. ( B \ C ) ) = ( A \ C ) )