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

Theorem en2other2 8458
 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 8457 . . . . . . 7
2 prcom 4041 . . . . . . 7
31, 2syl6eq 2521 . . . . . 6
43difeq1d 3539 . . . . 5
5 difprsnss 4098 . . . . 5
64, 5syl6eqss 3468 . . . 4
7 simpl 464 . . . . . 6
8 1onn 7358 . . . . . . . . . 10
98a1i 11 . . . . . . . . 9
10 simpr 468 . . . . . . . . . 10
11 df-2o 7201 . . . . . . . . . 10
1210, 11syl6breq 4435 . . . . . . . . 9
13 dif1en 7822 . . . . . . . . 9
149, 12, 7, 13syl3anc 1292 . . . . . . . 8
15 en1uniel 7659 . . . . . . . 8
16 eldifsni 4089 . . . . . . . 8
1714, 15, 163syl 18 . . . . . . 7
1817necomd 2698 . . . . . 6
19 eldifsn 4088 . . . . . 6
207, 18, 19sylanbrc 677 . . . . 5
2120snssd 4108 . . . 4
226, 21eqssd 3435 . . 3
2322unieqd 4200 . 2
24 unisng 4206 . . 3