Metamath Proof Explorer

Theorem dftr4

Description: An alternate way of defining a transitive class. Definition of Enderton p. 71. (Contributed by NM, 29-Aug-1993)

Ref Expression
Assertion dftr4 
|- ( Tr A <-> A C_ ~P A )

Proof

Step Hyp Ref Expression
1 df-tr 
 |-  ( Tr A <-> U. A C_ A )
2 sspwuni 
 |-  ( A C_ ~P A <-> U. A C_ A )
3 1 2 bitr4i 
 |-  ( Tr A <-> A C_ ~P A )