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

Theorem uneqdifeq 4441
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 4133 . . . . 5 (𝐵𝐴) = (𝐴𝐵)
2 eqtr 2846 . . . . . . 7 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → (𝐵𝐴) = 𝐶)
32eqcomd 2832 . . . . . 6 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → 𝐶 = (𝐵𝐴))
4 difeq1 4096 . . . . . . 7 (𝐶 = (𝐵𝐴) → (𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴))
5 difun2 4432 . . . . . . 7 ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)
6 eqtr 2846 . . . . . . . 8 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → (𝐶𝐴) = (𝐵𝐴))
7 incom 4182 . . . . . . . . . . 11 (𝐴𝐵) = (𝐵𝐴)
87eqeq1i 2831 . . . . . . . . . 10 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
9 disj3 4406 . . . . . . . . . 10 ((𝐵𝐴) = ∅ ↔ 𝐵 = (𝐵𝐴))
108, 9bitri 276 . . . . . . . . 9 ((𝐴𝐵) = ∅ ↔ 𝐵 = (𝐵𝐴))
11 eqtr 2846 . . . . . . . . . . 11 (((𝐶𝐴) = (𝐵𝐴) ∧ (𝐵𝐴) = 𝐵) → (𝐶𝐴) = 𝐵)
1211expcom 414 . . . . . . . . . 10 ((𝐵𝐴) = 𝐵 → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1312eqcoms 2834 . . . . . . . . 9 (𝐵 = (𝐵𝐴) → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
1410, 13sylbi 218 . . . . . . . 8 ((𝐴𝐵) = ∅ → ((𝐶𝐴) = (𝐵𝐴) → (𝐶𝐴) = 𝐵))
156, 14syl5com 31 . . . . . . 7 (((𝐶𝐴) = ((𝐵𝐴) ∖ 𝐴) ∧ ((𝐵𝐴) ∖ 𝐴) = (𝐵𝐴)) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
164, 5, 15sylancl 586 . . . . . 6 (𝐶 = (𝐵𝐴) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
173, 16syl 17 . . . . 5 (((𝐵𝐴) = (𝐴𝐵) ∧ (𝐴𝐵) = 𝐶) → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
181, 17mpan 686 . . . 4 ((𝐴𝐵) = 𝐶 → ((𝐴𝐵) = ∅ → (𝐶𝐴) = 𝐵))
1918com12 32 . . 3 ((𝐴𝐵) = ∅ → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
2019adantl 482 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 → (𝐶𝐴) = 𝐵))
21 simpl 483 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐴𝐶)
22 difssd 4113 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐶)
23 sseq1 3996 . . . . . . . 8 ((𝐶𝐴) = 𝐵 → ((𝐶𝐴) ⊆ 𝐶𝐵𝐶))
2422, 23mpbid 233 . . . . . . 7 ((𝐶𝐴) = 𝐵𝐵𝐶)
2524adantl 482 . . . . . 6 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐵𝐶)
2621, 25unssd 4166 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) ⊆ 𝐶)
27 eqimss 4027 . . . . . . 7 ((𝐶𝐴) = 𝐵 → (𝐶𝐴) ⊆ 𝐵)
28 ssundif 4436 . . . . . . 7 (𝐶 ⊆ (𝐴𝐵) ↔ (𝐶𝐴) ⊆ 𝐵)
2927, 28sylibr 235 . . . . . 6 ((𝐶𝐴) = 𝐵𝐶 ⊆ (𝐴𝐵))
3029adantl 482 . . . . 5 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → 𝐶 ⊆ (𝐴𝐵))
3126, 30eqssd 3988 . . . 4 ((𝐴𝐶 ∧ (𝐶𝐴) = 𝐵) → (𝐴𝐵) = 𝐶)
3231ex 413 . . 3 (𝐴𝐶 → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3332adantr 481 . 2 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐶𝐴) = 𝐵 → (𝐴𝐵) = 𝐶))
3420, 33impbid 213 1 ((𝐴𝐶 ∧ (𝐴𝐵) = ∅) → ((𝐴𝐵) = 𝐶 ↔ (𝐶𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296
This theorem is referenced by:  fzdifsuc  12957  hashbclem  13800  lecldbas  21743  conndisj  21940  ptuncnv  22331  ptunhmeo  22332  cldsubg  22634  icopnfcld  23291  iocmnfcld  23292  voliunlem1  24066  icombl  24080  ioombl  24081  uniioombllem4  24102  ismbf3d  24170  lhop  24528  symgcom  30641  f1resfz0f1d  32245  subfacp1lem3  32313  subfacp1lem5  32315  pconnconn  32362  cvmscld  32404
  Copyright terms: Public domain W3C validator