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

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 ↔ ∀ x ∈ A x ⊆ A

Proof

Step Hyp Ref Expression
1 dftr5 ⊢ Tr ⁡ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A
2 dfss3 ⊢ x ⊆ A ↔ ∀ y ∈ x y ∈ A
3 2 ralbii ⊢ ∀ x ∈ A x ⊆ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A
4 1 3 bitr4i ⊢ Tr ⁡ A ↔ ∀ x ∈ A x ⊆ A