Metamath Proof Explorer

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 ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
2 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
3 1 2 orbi12i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∨ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
4 pm4.42 ⊢ ( 𝑥 ∈ 𝐴 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
5 3 4 bitr4i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∨ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ) ↔ 𝑥 ∈ 𝐴 )
6 5 uneqri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴