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

Metamath Proof Explorer

Theorem trv

Description: The universe is transitive. (Contributed by NM, 14-Sep-2003)

Ref Expression
Assertion trv 
|- Tr _V

Proof

Step Hyp Ref Expression
1 ssv 
 |-  U. _V C_ _V
2 df-tr 
 |-  ( Tr _V <-> U. _V C_ _V )
3 1 2 mpbir 
 |-  Tr _V