Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneqdifeq Structured version   Visualization version   GIF version

Theorem uneqdifeq 4009
 Description: Two ways to say that 𝐴 and 𝐵 partition 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). (Contributed by FL, 17-Nov-2008.) (Proof shortened by JJ, 14-Jul-2021.)
Assertion
Ref Expression
uneqdifeq ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))

Proof of Theorem uneqdifeq
StepHypRef Expression
1 uncom 3719 . . . . 5 (𝐵𝐴) = (𝐴𝐵)
2 eqtr 2629 . . . . . . 7 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → (𝐵𝐴) = 𝐶)
32eqcomd 2616 . . . . . 6 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → 𝐶 = (𝐵𝐴))
4 difeq1 3683 . . . . . . 7 (𝐶 = (𝐵𝐴) → (𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴))
5 difun2 4000 . . . . . . 7 ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)
6 eqtr 2629 . . . . . . . 8 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → (𝐶𝐴) = (𝐵𝐴))
7 incom 3767 . . . . . . . . . . 11 (𝐴𝐵) = (𝐵𝐴)
87eqeq1i 2615 . . . . . . . . . 10 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
9 disj3 3973 . . . . . . . . . 10 ((𝐵𝐴) = ∅ ↔ 𝐵 = (𝐵𝐴))
108, 9bitri 263 . . . . . . . . 9 ((𝐴𝐵) = ∅ ↔ 𝐵 = (𝐵𝐴))
11 eqtr 2629 . . . . . . . . . . 11 (((𝐶𝐴) = (𝐵𝐴) ∧ (𝐵𝐴) = 𝐵) → (𝐶𝐴) = 𝐵)
1211expcom 450 . . . . . . . . . 10 ((𝐵𝐴) = 𝐵 → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1312eqcoms 2618 . . . . . . . . 9 (𝐵 = (𝐵𝐴) → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1410, 13sylbi 206 . . . . . . . 8 ((𝐴𝐵) = ∅ → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
156, 14syl5com 31 . . . . . . 7 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
164, 5, 15sylancl 693 . . . . . 6 (𝐶 = (𝐵𝐴) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
173, 16syl 17 . . . . 5 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
181, 17mpan 702 . . . 4 ((𝐴𝐵) = 𝐶 → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
1918com12 32 . . 3 ((𝐴𝐵) = ∅ → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
2019adantl 481 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
21 simpl 472 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐴𝐶)
22 difssd 3700 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐶)
23 sseq1 3589 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → ((𝐶𝐴) ⊆ 𝐶𝐵𝐶))
2422, 23mpbid 221 . . . . . . 7 ((𝐶𝐴) = 𝐵𝐵𝐶)
2524adantl 481 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐵𝐶)
2621, 25unssd 3751 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) ⊆ 𝐶)
27 eqimss 3620 . . . . . . 7 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐵)
28 ssundif 4004 . . . . . . 7 (𝐶 ⊆ (𝐴𝐵) ↔ (𝐶𝐴) ⊆ 𝐵)
2927, 28sylibr 223 . . . . . 6 ((𝐶𝐴) = 𝐵𝐶 ⊆ (𝐴𝐵))
3029adantl 481 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐶 ⊆ (𝐴𝐵))
3126, 30eqssd 3585 . . . 4 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) = 𝐶)
3231ex 449 . . 3 (𝐴𝐶 → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3332adantr 480 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3420, 33impbid 201 1 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875 This theorem is referenced by:  fzdifsuc  12270  hashbclem  13093  lecldbas  20833  conndisj  21029  ptuncnv  21420  ptunhmeo  21421  cldsubg  21724  icopnfcld  22381  iocmnfcld  22382  voliunlem1  23125  icombl  23139  ioombl  23140  uniioombllem4  23160  ismbf3d  23227  lhop  23583  subfacp1lem3  30418  subfacp1lem5  30420  pconcon  30467  cvmscld  30509
 Copyright terms: Public domain W3C validator