Theorem inundif

Description: The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	inundif	|- ( ( A i^i B ) u. ( A \ B ) ) = A

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		eldif	|- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	1 2	orbi12i	|- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
4		pm4.42	|- ( x e. A <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
5	3 4	bitr4i	|- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> x e. A )
6	5	uneqri	|- ( ( A i^i B ) u. ( A \ B ) ) = A