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 
|- ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) = ( C i^i B ) )

Proof

Step Hyp Ref Expression
1 indif1 
 |-  ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )
2 1 eqeq1i 
 |-  ( ( ( A \ C ) i^i B ) = (/) <-> ( ( A i^i B ) \ C ) = (/) )
3 ssdif0 
 |-  ( ( A i^i B ) C_ C <-> ( ( A i^i B ) \ C ) = (/) )
4 2 3 sylbb2 
 |-  ( ( ( A \ C ) i^i B ) = (/) -> ( A i^i B ) C_ C )
5 4 adantr 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) C_ C )
6 inss2 
 |-  ( A i^i B ) C_ B
7 6 a1i 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) C_ B )
8 5 7 ssind 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) C_ ( C i^i B ) )
9 indif1 
 |-  ( ( C \ A ) i^i B ) = ( ( C i^i B ) \ A )
10 9 eqeq1i 
 |-  ( ( ( C \ A ) i^i B ) = (/) <-> ( ( C i^i B ) \ A ) = (/) )
11 ssdif0 
 |-  ( ( C i^i B ) C_ A <-> ( ( C i^i B ) \ A ) = (/) )
12 10 11 sylbb2 
 |-  ( ( ( C \ A ) i^i B ) = (/) -> ( C i^i B ) C_ A )
13 12 adantl 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( C i^i B ) C_ A )
14 inss2 
 |-  ( C i^i B ) C_ B
15 14 a1i 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( C i^i B ) C_ B )
16 13 15 ssind 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( C i^i B ) C_ ( A i^i B ) )
17 8 16 eqssd 
 |-  ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) = ( C i^i B ) )