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 simpl 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( C i^i B ) = (/) )
9 disj3 
 |-  ( ( C i^i B ) = (/) <-> C = ( C \ B ) )
10 eqcom 
 |-  ( C = ( C \ B ) <-> ( C \ B ) = C )
11 9 10 bitri 
 |-  ( ( C i^i B ) = (/) <-> ( C \ B ) = C )
12 8 11 sylib 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( C \ B ) = C )
13 difeq1 
 |-  ( ( C u. B ) = ( A u. B ) -> ( ( C u. B ) \ B ) = ( ( A u. B ) \ B ) )
14 difun2 
 |-  ( ( C u. B ) \ B ) = ( C \ B )
15 difun2 
 |-  ( ( A u. B ) \ B ) = ( A \ B )
16 13 14 15 3eqtr3g 
 |-  ( ( C u. B ) = ( A u. B ) -> ( C \ B ) = ( A \ B ) )
17 16 eqeq1d 
 |-  ( ( C u. B ) = ( A u. B ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
18 17 adantl 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
19 12 18 mpbid 
 |-  ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( A \ B ) = C )
20 7 19 impbii 
 |-  ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )