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

Theorem uneqdifeq 3916
Description: Two ways to say that and partition (when and don't overlap and is a part of ). (Contributed by FL, 17-Nov-2008.)
Assertion
Ref Expression
uneqdifeq

Proof of Theorem uneqdifeq
StepHypRef Expression
1 uncom 3647 . . . . 5
2 eqtr 2483 . . . . . . 7
32eqcomd 2465 . . . . . 6
4 difeq1 3614 . . . . . . 7
5 difun2 3907 . . . . . . 7
6 eqtr 2483 . . . . . . . 8
7 incom 3690 . . . . . . . . . . 11
87eqeq1i 2464 . . . . . . . . . 10
9 disj3 3871 . . . . . . . . . 10
108, 9bitri 249 . . . . . . . . 9
11 eqtr 2483 . . . . . . . . . . 11
1211expcom 435 . . . . . . . . . 10
1312eqcoms 2469 . . . . . . . . 9
1410, 13sylbi 195 . . . . . . . 8
156, 14syl5com 30 . . . . . . 7
164, 5, 15sylancl 662 . . . . . 6
173, 16syl 16 . . . . 5
181, 17mpan 670 . . . 4
1918com12 31 . . 3
2019adantl 466 . 2
21 difss 3630 . . . . . . . 8
22 sseq1 3524 . . . . . . . . 9
23 unss 3677 . . . . . . . . . . 11
2423biimpi 194 . . . . . . . . . 10
2524expcom 435 . . . . . . . . 9
2622, 25syl6bi 228 . . . . . . . 8
2721, 26mpi 17 . . . . . . 7
2827com12 31 . . . . . 6
2928adantr 465 . . . . 5
3029imp 429 . . . 4
31 eqimss 3555 . . . . . . 7
3231adantl 466 . . . . . 6
33 ssundif 3911 . . . . . 6
3432, 33sylibr 212 . . . . 5
3534adantlr 714 . . . 4
3630, 35eqssd 3520 . . 3
3736ex 434 . 2
3820, 37impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  \cdif 3472  u.cun 3473  i^icin 3474  C_wss 3475   c0 3784
This theorem is referenced by:  fzdifsuc  11768  hashbclem  12501  lecldbas  19720  conndisj  19917  ptuncnv  20308  ptunhmeo  20309  cldsubg  20609  icopnfcld  21275  iocmnfcld  21276  voliunlem1  21960  icombl  21974  ioombl  21975  uniioombllem4  21995  ismbf3d  22061  lhop  22417  subfacp1lem3  28626  subfacp1lem5  28628  pconcon  28676  cvmscld  28718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785
  Copyright terms: Public domain W3C validator