Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  uneqdifeqim Structured version   Unicode version

Theorem uneqdifeqim 3302
 Description: Two ways that and can "partition" (when and don't overlap and is a part of ). In classical logic, the second implication would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.)
Assertion
Ref Expression
uneqdifeqim

Proof of Theorem uneqdifeqim
StepHypRef Expression
1 uncom 3081 . . . 4
2 eqtr 2054 . . . . . 6
32eqcomd 2042 . . . . 5
4 difeq1 3049 . . . . . 6
5 difun2 3296 . . . . . 6
6 eqtr 2054 . . . . . . 7
7 incom 3123 . . . . . . . . . 10
87eqeq1i 2044 . . . . . . . . 9
9 disj3 3266 . . . . . . . . 9
108, 9bitri 173 . . . . . . . 8
11 eqtr 2054 . . . . . . . . . 10
1211expcom 109 . . . . . . . . 9
1312eqcoms 2040 . . . . . . . 8
1410, 13sylbi 114 . . . . . . 7
156, 14syl5com 26 . . . . . 6
164, 5, 15sylancl 392 . . . . 5
173, 16syl 14 . . . 4
181, 17mpan 400 . . 3
1918com12 27 . 2