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 ( ( 𝐴𝐵 ) = 𝐶 ↔ ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 ( ( 𝐴𝐵 ) = 𝐶 → ( ( 𝐴𝐵 ) ∩ 𝐵 ) = ( 𝐶𝐵 ) )
2 disjdifr ( ( 𝐴𝐵 ) ∩ 𝐵 ) = ∅
3 1 2 eqtr3di ( ( 𝐴𝐵 ) = 𝐶 → ( 𝐶𝐵 ) = ∅ )
4 uneq1 ( ( 𝐴𝐵 ) = 𝐶 → ( ( 𝐴𝐵 ) ∪ 𝐵 ) = ( 𝐶𝐵 ) )
5 undif1 ( ( 𝐴𝐵 ) ∪ 𝐵 ) = ( 𝐴𝐵 )
6 4 5 eqtr3di ( ( 𝐴𝐵 ) = 𝐶 → ( 𝐶𝐵 ) = ( 𝐴𝐵 ) )
7 3 6 jca ( ( 𝐴𝐵 ) = 𝐶 → ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) )
8 simpl ( ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) → ( 𝐶𝐵 ) = ∅ )
9 disj3 ( ( 𝐶𝐵 ) = ∅ ↔ 𝐶 = ( 𝐶𝐵 ) )
10 eqcom ( 𝐶 = ( 𝐶𝐵 ) ↔ ( 𝐶𝐵 ) = 𝐶 )
11 9 10 bitri ( ( 𝐶𝐵 ) = ∅ ↔ ( 𝐶𝐵 ) = 𝐶 )
12 8 11 sylib ( ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) → ( 𝐶𝐵 ) = 𝐶 )
13 difeq1 ( ( 𝐶𝐵 ) = ( 𝐴𝐵 ) → ( ( 𝐶𝐵 ) ∖ 𝐵 ) = ( ( 𝐴𝐵 ) ∖ 𝐵 ) )
14 difun2 ( ( 𝐶𝐵 ) ∖ 𝐵 ) = ( 𝐶𝐵 )
15 difun2 ( ( 𝐴𝐵 ) ∖ 𝐵 ) = ( 𝐴𝐵 )
16 13 14 15 3eqtr3g ( ( 𝐶𝐵 ) = ( 𝐴𝐵 ) → ( 𝐶𝐵 ) = ( 𝐴𝐵 ) )
17 16 eqeq1d ( ( 𝐶𝐵 ) = ( 𝐴𝐵 ) → ( ( 𝐶𝐵 ) = 𝐶 ↔ ( 𝐴𝐵 ) = 𝐶 ) )
18 17 adantl ( ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) → ( ( 𝐶𝐵 ) = 𝐶 ↔ ( 𝐴𝐵 ) = 𝐶 ) )
19 12 18 mpbid ( ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) → ( 𝐴𝐵 ) = 𝐶 )
20 7 19 impbii ( ( 𝐴𝐵 ) = 𝐶 ↔ ( ( 𝐶𝐵 ) = ∅ ∧ ( 𝐶𝐵 ) = ( 𝐴𝐵 ) ) )