Metamath Proof Explorer


Theorem undif3

Description: An equality involving class union and class difference. The first equality of Exercise 13 of TakeutiZaring p. 22. (Contributed by Alan Sare, 17-Apr-2012) (Proof shortened by JJ, 13-Jul-2021)

Ref Expression
Assertion undif3 ( 𝐴 ∪ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ∖ ( 𝐶𝐴 ) )

Proof

Step Hyp Ref Expression
1 elun ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
2 pm4.53 ( ¬ ( 𝑥𝐶 ∧ ¬ 𝑥𝐴 ) ↔ ( ¬ 𝑥𝐶𝑥𝐴 ) )
3 eldif ( 𝑥 ∈ ( 𝐶𝐴 ) ↔ ( 𝑥𝐶 ∧ ¬ 𝑥𝐴 ) )
4 2 3 xchnxbir ( ¬ 𝑥 ∈ ( 𝐶𝐴 ) ↔ ( ¬ 𝑥𝐶𝑥𝐴 ) )
5 1 4 anbi12i ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐶𝐴 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( ¬ 𝑥𝐶𝑥𝐴 ) ) )
6 eldif ( 𝑥 ∈ ( ( 𝐴𝐵 ) ∖ ( 𝐶𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐶𝐴 ) ) )
7 elun ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵𝐶 ) ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐵𝐶 ) ) )
8 eldif ( 𝑥 ∈ ( 𝐵𝐶 ) ↔ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) )
9 8 orbi2i ( ( 𝑥𝐴𝑥 ∈ ( 𝐵𝐶 ) ) ↔ ( 𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) ) )
10 ordi ( ( 𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑥𝐴 ∨ ¬ 𝑥𝐶 ) ) )
11 orcom ( ( 𝑥𝐴 ∨ ¬ 𝑥𝐶 ) ↔ ( ¬ 𝑥𝐶𝑥𝐴 ) )
12 11 anbi2i ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( 𝑥𝐴 ∨ ¬ 𝑥𝐶 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( ¬ 𝑥𝐶𝑥𝐴 ) ) )
13 10 12 bitri ( ( 𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( ¬ 𝑥𝐶𝑥𝐴 ) ) )
14 7 9 13 3bitri ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵𝐶 ) ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ( ¬ 𝑥𝐶𝑥𝐴 ) ) )
15 5 6 14 3bitr4ri ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴𝐵 ) ∖ ( 𝐶𝐴 ) ) )
16 15 eqriv ( 𝐴 ∪ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ∖ ( 𝐶𝐴 ) )