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

Theorem uneqdifeq 4423
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 4087 . . . . 5 (𝐵𝐴) = (𝐴𝐵)
2 eqtr 2761 . . . . . . 7 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → (𝐵𝐴) = 𝐶)
32eqcomd 2744 . . . . . 6 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → 𝐶 = (𝐵𝐴))
4 difeq1 4050 . . . . . . 7 (𝐶 = (𝐵𝐴) → (𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴))
5 difun2 4414 . . . . . . 7 ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)
6 eqtr 2761 . . . . . . . 8 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → (𝐶𝐴) = (𝐵𝐴))
7 incom 4135 . . . . . . . . . . 11 (𝐴𝐵) = (𝐵𝐴)
87eqeq1i 2743 . . . . . . . . . 10 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
9 disj3 4387 . . . . . . . . . 10 ((𝐵𝐴) = ∅ ↔ 𝐵 = (𝐵𝐴))
108, 9bitri 274 . . . . . . . . 9 ((𝐴𝐵) = ∅ ↔ 𝐵 = (𝐵𝐴))
11 eqtr 2761 . . . . . . . . . . 11 (((𝐶𝐴) = (𝐵𝐴) ∧ (𝐵𝐴) = 𝐵) → (𝐶𝐴) = 𝐵)
1211expcom 414 . . . . . . . . . 10 ((𝐵𝐴) = 𝐵 → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1312eqcoms 2746 . . . . . . . . 9 (𝐵 = (𝐵𝐴) → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1410, 13sylbi 216 . . . . . . . 8 ((𝐴𝐵) = ∅ → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
156, 14syl5com 31 . . . . . . 7 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
164, 5, 15sylancl 586 . . . . . 6 (𝐶 = (𝐵𝐴) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
173, 16syl 17 . . . . 5 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
181, 17mpan 687 . . . 4 ((𝐴𝐵) = 𝐶 → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
1918com12 32 . . 3 ((𝐴𝐵) = ∅ → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
2019adantl 482 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
21 simpl 483 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐴𝐶)
22 difssd 4067 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐶)
23 sseq1 3946 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → ((𝐶𝐴) ⊆ 𝐶𝐵𝐶))
2422, 23mpbid 231 . . . . . . 7 ((𝐶𝐴) = 𝐵𝐵𝐶)
2524adantl 482 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐵𝐶)
2621, 25unssd 4120 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) ⊆ 𝐶)
27 eqimss 3977 . . . . . . 7 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐵)
28 ssundif 4418 . . . . . . 7 (𝐶 ⊆ (𝐴𝐵) ↔ (𝐶𝐴) ⊆ 𝐵)
2927, 28sylibr 233 . . . . . 6 ((𝐶𝐴) = 𝐵𝐶 ⊆ (𝐴𝐵))
3029adantl 482 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐶 ⊆ (𝐴𝐵))
3126, 30eqssd 3938 . . . 4 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) = 𝐶)
3231ex 413 . . 3 (𝐴𝐶 → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3332adantr 481 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3420, 33impbid 211 1 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257
This theorem is referenced by:  fzdifsuc  13316  hashbclem  14164  lecldbas  22370  conndisj  22567  ptuncnv  22958  ptunhmeo  22959  cldsubg  23262  icopnfcld  23931  iocmnfcld  23932  voliunlem1  24714  icombl  24728  ioombl  24729  uniioombllem4  24750  ismbf3d  24818  lhop  25180  symgcom  31352  f1resfz0f1d  33072  subfacp1lem3  33144  subfacp1lem5  33146  pconnconn  33193  cvmscld  33235
  Copyright terms: Public domain W3C validator