This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difininv

Description: Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021)

Ref Expression
Assertion difininv ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ( 𝐶 ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 indif1 ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 )
2 1 eqeq1i ⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ )
3 ssdif0 ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ )
4 2 3 sylbb2 ⊢ ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
5 4 adantr ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
6 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
7 6 a1i ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
8 5 7 ssind ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐵 ) )
9 indif1 ⊢ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 )
10 9 eqeq1i ⊢ ( ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ↔ ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 ) = ∅ )
11 ssdif0 ⊢ ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ( 𝐶 ∩ 𝐵 ) ∖ 𝐴 ) = ∅ )
12 10 11 sylbb2 ⊢ ( ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 )
13 12 adantl ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐴 )
14 inss2 ⊢ ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵
15 14 a1i ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 )
16 13 15 ssind ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
17 8 16 eqssd ⊢ ( ( ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶 ∖ 𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ( 𝐶 ∩ 𝐵 ) )