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

Theorem posn 4914
 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 4766 . . 3
2 breq2 4421 . . . . . . . . . . . 12
32anbi2d 708 . . . . . . . . . . 11
4 breq2 4421 . . . . . . . . . . 11
53, 4imbi12d 321 . . . . . . . . . 10
65anbi2d 708 . . . . . . . . 9
76ralsng 4028 . . . . . . . 8
87ralbidv 2862 . . . . . . 7
9 simpl 458 . . . . . . . . . . 11
10 breq2 4421 . . . . . . . . . . 11
119, 10syl5ib 222 . . . . . . . . . 10
1211biantrud 509 . . . . . . . . 9
1312bicomd 204 . . . . . . . 8
1413ralsng 4028 . . . . . . 7
158, 14bitrd 256 . . . . . 6
1615ralbidv 2862 . . . . 5
17 breq12 4422 . . . . . . . 8
1817anidms 649 . . . . . . 7
1918notbid 295 . . . . . 6
2019ralsng 4028 . . . . 5
2116, 20bitrd 256 . . . 4