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		incom	|- ( B i^i ( A \ B ) ) = ( ( A \ B ) i^i B )
2		disjdif	|- ( B i^i ( A \ B ) ) = (/)
3	1 2	eqtr3i	|- ( ( A \ B ) i^i B ) = (/)
4		ineq1	|- ( ( A \ B ) = C -> ( ( A \ B ) i^i B ) = ( C i^i B ) )
5	3 4	syl5reqr	|- ( ( A \ B ) = C -> ( C i^i B ) = (/) )
6		undif1	|- ( ( A \ B ) u. B ) = ( A u. B )
7		uneq1	|- ( ( A \ B ) = C -> ( ( A \ B ) u. B ) = ( C u. B ) )
8	6 7	syl5reqr	|- ( ( A \ B ) = C -> ( C u. B ) = ( A u. B ) )
9	5 8	jca	|- ( ( A \ B ) = C -> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )
10		simpl	|- ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( C i^i B ) = (/) )
11		disj3	|- ( ( C i^i B ) = (/) <-> C = ( C \ B ) )
12		eqcom	|- ( C = ( C \ B ) <-> ( C \ B ) = C )
13	11 12	bitri	|- ( ( C i^i B ) = (/) <-> ( C \ B ) = C )
14	10 13	sylib	|- ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( C \ B ) = C )
15		difeq1	|- ( ( C u. B ) = ( A u. B ) -> ( ( C u. B ) \ B ) = ( ( A u. B ) \ B ) )
16		difun2	|- ( ( C u. B ) \ B ) = ( C \ B )
17		difun2	|- ( ( A u. B ) \ B ) = ( A \ B )
18	15 16 17	3eqtr3g	|- ( ( C u. B ) = ( A u. B ) -> ( C \ B ) = ( A \ B ) )
19	18	eqeq1d	|- ( ( C u. B ) = ( A u. B ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
20	19	adantl	|- ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( ( C \ B ) = C <-> ( A \ B ) = C ) )
21	14 20	mpbid	|- ( ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) -> ( A \ B ) = C )
22	9 21	impbii	|- ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )