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 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dftr5	⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 )
2		dfss3	⊢ ( 𝑥 ⊆ 𝐴 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 )
4	1 3	bitr4i	⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 )