Metamath Proof Explorer

Theorem dftr3

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

Ref Expression
Assertion dftr3 
|- ( Tr A <-> A. x e. A x C_ A )

Proof

Step Hyp Ref Expression
1 dftr5 
 |-  ( Tr A <-> A. x e. A A. y e. x y e. A )
2 dfss3 
 |-  ( x C_ A <-> A. y e. x y e. A )
3 2 ralbii 
 |-  ( A. x e. A x C_ A <-> A. x e. A A. y e. x y e. A )
4 1 3 bitr4i 
 |-  ( Tr A <-> A. x e. A x C_ A )