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

Metamath Proof Explorer

Theorem dftr2

Description: An alternate way of defining a transitive class. Exercise 7 of TakeutiZaring p. 40. Using dftr2c instead may avoid dependences on ax-11 . (Contributed by NM, 24-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		df-ss	⊢ ( ∪ 𝐴 ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ 𝐴 ) )
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 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )