Metamath Proof Explorer


Theorem difin2

Description: Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion difin2 ( 𝐴𝐶 → ( 𝐴𝐵 ) = ( ( 𝐶𝐵 ) ∩ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssel ( 𝐴𝐶 → ( 𝑥𝐴𝑥𝐶 ) )
2 1 pm4.71d ( 𝐴𝐶 → ( 𝑥𝐴 ↔ ( 𝑥𝐴𝑥𝐶 ) ) )
3 2 anbi1d ( 𝐴𝐶 → ( ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ↔ ( ( 𝑥𝐴𝑥𝐶 ) ∧ ¬ 𝑥𝐵 ) ) )
4 eldif ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
5 elin ( 𝑥 ∈ ( ( 𝐶𝐵 ) ∩ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝐶𝐵 ) ∧ 𝑥𝐴 ) )
6 eldif ( 𝑥 ∈ ( 𝐶𝐵 ) ↔ ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) )
7 6 anbi1i ( ( 𝑥 ∈ ( 𝐶𝐵 ) ∧ 𝑥𝐴 ) ↔ ( ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ∧ 𝑥𝐴 ) )
8 ancom ( ( ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ∧ 𝑥𝐴 ) ↔ ( 𝑥𝐴 ∧ ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ) )
9 anass ( ( ( 𝑥𝐴𝑥𝐶 ) ∧ ¬ 𝑥𝐵 ) ↔ ( 𝑥𝐴 ∧ ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ) )
10 8 9 bitr4i ( ( ( 𝑥𝐶 ∧ ¬ 𝑥𝐵 ) ∧ 𝑥𝐴 ) ↔ ( ( 𝑥𝐴𝑥𝐶 ) ∧ ¬ 𝑥𝐵 ) )
11 5 7 10 3bitri ( 𝑥 ∈ ( ( 𝐶𝐵 ) ∩ 𝐴 ) ↔ ( ( 𝑥𝐴𝑥𝐶 ) ∧ ¬ 𝑥𝐵 ) )
12 3 4 11 3bitr4g ( 𝐴𝐶 → ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ 𝑥 ∈ ( ( 𝐶𝐵 ) ∩ 𝐴 ) ) )
13 12 eqrdv ( 𝐴𝐶 → ( 𝐴𝐵 ) = ( ( 𝐶𝐵 ) ∩ 𝐴 ) )