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 ) ) )