New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  uneqdifeq GIF version

Theorem uneqdifeq 3638
 Description: Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C). (Contributed by FL, 17-Nov-2008.)
Assertion
Ref Expression
uneqdifeq ((A C (AB) = ) → ((AB) = C ↔ (C A) = B))

Proof of Theorem uneqdifeq
StepHypRef Expression
1 uncom 3408 . . . . 5 (BA) = (AB)
2 eqtr 2370 . . . . . . 7 (((BA) = (AB) (AB) = C) → (BA) = C)
32eqcomd 2358 . . . . . 6 (((BA) = (AB) (AB) = C) → C = (BA))
4 difeq1 3246 . . . . . . 7 (C = (BA) → (C A) = ((BA) A))
5 difun2 3629 . . . . . . 7 ((BA) A) = (B A)
6 eqtr 2370 . . . . . . . 8 (((C A) = ((BA) A) ((BA) A) = (B A)) → (C A) = (B A))
7 incom 3448 . . . . . . . . . . 11 (AB) = (BA)
87eqeq1i 2360 . . . . . . . . . 10 ((AB) = ↔ (BA) = )
9 disj3 3595 . . . . . . . . . 10 ((BA) = B = (B A))
108, 9bitri 240 . . . . . . . . 9 ((AB) = B = (B A))
11 eqtr 2370 . . . . . . . . . . 11 (((C A) = (B A) (B A) = B) → (C A) = B)
1211expcom 424 . . . . . . . . . 10 ((B A) = B → ((C A) = (B A) → (C A) = B))
1312eqcoms 2356 . . . . . . . . 9 (B = (B A) → ((C A) = (B A) → (C A) = B))
1410, 13sylbi 187 . . . . . . . 8 ((AB) = → ((C A) = (B A) → (C A) = B))
156, 14syl5com 26 . . . . . . 7 (((C A) = ((BA) A) ((BA) A) = (B A)) → ((AB) = → (C A) = B))
164, 5, 15sylancl 643 . . . . . 6 (C = (BA) → ((AB) = → (C A) = B))
173, 16syl 15 . . . . 5 (((BA) = (AB) (AB) = C) → ((AB) = → (C A) = B))
181, 17mpan 651 . . . 4 ((AB) = C → ((AB) = → (C A) = B))
1918com12 27 . . 3 ((AB) = → ((AB) = C → (C A) = B))
2019adantl 452 . 2 ((A C (AB) = ) → ((AB) = C → (C A) = B))
21 difss 3393 . . . . . . . 8 (C A) C
22 sseq1 3292 . . . . . . . . 9 ((C A) = B → ((C A) CB C))
23 unss 3437 . . . . . . . . . . 11 ((A C B C) ↔ (AB) C)
2423biimpi 186 . . . . . . . . . 10 ((A C B C) → (AB) C)
2524expcom 424 . . . . . . . . 9 (B C → (A C → (AB) C))
2622, 25syl6bi 219 . . . . . . . 8 ((C A) = B → ((C A) C → (A C → (AB) C)))
2721, 26mpi 16 . . . . . . 7 ((C A) = B → (A C → (AB) C))
2827com12 27 . . . . . 6 (A C → ((C A) = B → (AB) C))
2928adantr 451 . . . . 5 ((A C (AB) = ) → ((C A) = B → (AB) C))
3029imp 418 . . . 4 (((A C (AB) = ) (C A) = B) → (AB) C)
31 eqimss 3323 . . . . . . 7 ((C A) = B → (C A) B)
3231adantl 452 . . . . . 6 ((A C (C A) = B) → (C A) B)
33 ssundif 3633 . . . . . 6 (C (AB) ↔ (C A) B)
3432, 33sylibr 203 . . . . 5 ((A C (C A) = B) → C (AB))
3534adantlr 695 . . . 4 (((A C (AB) = ) (C A) = B) → C (AB))
3630, 35eqssd 3289 . . 3 (((A C (AB) = ) (C A) = B) → (AB) = C)
3736ex 423 . 2 ((A C (AB) = ) → ((C A) = B → (AB) = C))
3820, 37impbid 183 1 ((A C (AB) = ) → ((AB) = C ↔ (C A) = B))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊆ wss 3257  ∅c0 3550 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator