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 ( ( ( ( 𝐴𝐶 ) ∩ 𝐵 ) = ∅ ∧ ( ( 𝐶𝐴 ) ∩ 𝐵 ) = ∅ ) → ( 𝐴𝐵 ) = ( 𝐶𝐵 ) )