Theorem dftr2

Description: An alternate way of defining a transitive class. Exercise 7 of TakeutiZaring p. 40. (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dftr2	⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( ∪ 𝐴 ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴 ) )
2		df-tr	⊢ ( Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴 )
3		19.23v	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )
4		eluni	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
5	4	imbi1i	⊢ ( ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )
6	3 5	bitr4i	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴 ) )
7	6	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴 ) )
8	1 2 7	3bitr4i	⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )