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