Metamath Proof Explorer


Theorem iundifdif

Description: The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd . (Contributed by Thierry Arnoux, 4-Sep-2016)

Ref Expression
Hypotheses iundifdif.o O V
iundifdif.2 A 𝒫 O
Assertion iundifdif A A = O x A O x

Proof

Step Hyp Ref Expression
1 iundifdif.o O V
2 iundifdif.2 A 𝒫 O
3 iundif2 x A O x = O x A x
4 intiin A = x A x
5 4 difeq2i O A = O x A x
6 3 5 eqtr4i x A O x = O A
7 6 difeq2i O x A O x = O O A
8 2 jctl A A 𝒫 O A
9 intssuni2 A 𝒫 O A A 𝒫 O
10 unipw 𝒫 O = O
11 10 sseq2i A 𝒫 O A O
12 11 biimpi A 𝒫 O A O
13 8 9 12 3syl A A O
14 dfss4 A O O O A = A
15 13 14 sylib A O O A = A
16 7 15 eqtr2id A A = O x A O x