Theorem iundifdifd

Description: The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016)

	Ref	Expression
Assertion	iundifdifd	|- ( A C_ ~P O -> ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iundif2	|- U_ x e. A ( O \ x ) = ( O \ |^|_ x e. A x )
2		intiin	|- |^| A = |^|_ x e. A x
3	2	difeq2i	|- ( O \ |^| A ) = ( O \ |^|_ x e. A x )
4	1 3	eqtr4i	|- U_ x e. A ( O \ x ) = ( O \ |^| A )
5	4	difeq2i	|- ( O \ U_ x e. A ( O \ x ) ) = ( O \ ( O \ |^| A ) )
6		intssuni2	|- ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A C_ U. ~P O )
7		unipw	|- U. ~P O = O
8	6 7	sseqtrdi	|- ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A C_ O )
9		dfss4	|- ( |^| A C_ O <-> ( O \ ( O \ |^| A ) ) = |^| A )
10	8 9	sylib	|- ( ( A C_ ~P O /\ A =/= (/) ) -> ( O \ ( O \ |^| A ) ) = |^| A )
11	5 10	eqtr2id	|- ( ( A C_ ~P O /\ A =/= (/) ) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) )
12	11	ex	|- ( A C_ ~P O -> ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) ) )