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

Metamath Proof Explorer

Theorem difeq

Description: Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017)

Ref Expression
Assertion difeq 
|- ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( ( A \ B ) = C -> ( ( A \ B ) i^i B ) = ( C i^i B ) )
2 disjdifr 
 |-  ( ( A \ B ) i^i B ) = (/)
3 1 2 eqtr3di 
 |-  ( ( A \ B ) = C -> ( C i^i B ) = (/) )
4 uneq1 
 |-  ( ( A \ B ) = C -> ( ( A \ B ) u. B ) = ( C u. B ) )
5 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
6 4 5 eqtr3di 
 |-  ( ( A \ B ) = C -> ( C u. B ) = ( A u. B ) )
7 3 6 jca 
 |-  ( ( A \ B ) = C -> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )
8 disj3 
 |-  ( ( C i^i B ) = (/) <-> C = ( C \ B ) )
9 eqcom 
 |-  ( C = ( C \ B ) <-> ( C \ B ) = C )
10 8 9 bitri 
 |-  ( ( C i^i B ) = (/) <-> ( C \ B ) = C )
11 10 birani 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( C \ B ) = C )
12 difeq1 
 |-  ( ( C u. B ) = ( A u. B ) -> ( ( C u. B ) \ B ) = ( ( A u. B ) \ B ) )
13 difun2 
 |-  ( ( C u. B ) \ B ) = ( C \ B )
14 difun2 
 |-  ( ( A u. B ) \ B ) = ( A \ B )
15 12 13 14 3eqtr3g 
 |-  ( ( C u. B ) = ( A u. B ) -> ( C \ B ) = ( A \ B ) )
16 15 eqeq1d 
 |-  ( ( C u. B ) = ( A u. B ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
17 16 adantl 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
18 11 17 mpbid 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( A \ B ) = C )
19 7 18 impbii 
 |-  ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )