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

Theorem posn 4948
 Description: Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009.) (Revised by Mario Carneiro, 23-Apr-2015.)
Assertion
Ref Expression
posn

Proof of Theorem posn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-po 4505 . . 3
2 breq2 4218 . . . . . . . . . . . 12
32anbi2d 686 . . . . . . . . . . 11
4 breq2 4218 . . . . . . . . . . 11
53, 4imbi12d 313 . . . . . . . . . 10
65anbi2d 686 . . . . . . . . 9
76ralsng 3848 . . . . . . . 8
87ralbidv 2727 . . . . . . 7
9 simpl 445 . . . . . . . . . . 11
10 breq2 4218 . . . . . . . . . . 11
119, 10syl5ib 212 . . . . . . . . . 10
1211biantrud 495 . . . . . . . . 9
1312bicomd 194 . . . . . . . 8
1413ralsng 3848 . . . . . . 7
158, 14bitrd 246 . . . . . 6
1615ralbidv 2727 . . . . 5
17 breq12 4219 . . . . . . . 8
1817anidms 628 . . . . . . 7
1918notbid 287 . . . . . 6
2019ralsng 3848 . . . . 5
2116, 20bitrd 246 . . . 4
231, 22syl5bb 250 . 2
24 po0 4520 . . . . 5
25 snprc 3873 . . . . . 6
26 poeq2 4509 . . . . . 6
2725, 26sylbi 189 . . . . 5
2824, 27mpbiri 226 . . . 4