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

Theorem en2other2 6574
 Description: Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
Assertion
Ref Expression
en2other2

Proof of Theorem en2other2
StepHypRef Expression
1 en2eleq 6573 . . . . . . 7
2 prcom 3486 . . . . . . 7
31, 2syl6eq 2131 . . . . . 6
43difeq1d 3099 . . . . 5
5 difprsnss 3543 . . . . 5
64, 5syl6eqss 3058 . . . 4
7 simpl 107 . . . . . 6
8 1onn 6180 . . . . . . . . . 10
98a1i 9 . . . . . . . . 9
10 simpr 108 . . . . . . . . . 10
11 df-2o 6086 . . . . . . . . . 10
1210, 11syl6breq 3844 . . . . . . . . 9
13 dif1en 6435 . . . . . . . . 9
149, 12, 7, 13syl3anc 1170 . . . . . . . 8
15 en1uniel 6372 . . . . . . . 8
16 eldifsni 3537 . . . . . . . 8
1714, 15, 163syl 17 . . . . . . 7
1817necomd 2335 . . . . . 6
19 eldifsn 3535 . . . . . 6
207, 18, 19sylanbrc 408 . . . . 5
2120snssd 3550 . . . 4
226, 21eqssd 3025 . . 3
2322unieqd 3632 . 2
24 unisng 3638 . . 3