This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tr0

Description: The empty set is transitive. (Contributed by NM, 16-Sep-1993)

Ref Expression
Assertion tr0 
|- Tr (/)

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ ~P (/)
2 dftr4 
 |-  ( Tr (/) <-> (/) C_ ~P (/) )
3 1 2 mpbir 
 |-  Tr (/)