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

Metamath Proof Explorer

Theorem dftr5

Description: An alternate way of defining a transitive class. Definition 1.1 of Schloeder p. 1. (Contributed by NM, 20-Mar-2004) Avoid ax-11 . (Revised by BTernaryTau, 28-Dec-2024)

Ref Expression
Assertion dftr5 ( Tr 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 impexp ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
2 1 albii ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
3 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
4 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 ) )
5 2 3 4 3bitr2i ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 ) )
6 5 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 ) )
7 dftr2c ⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
8 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 ) )
9 6 7 8 3bitr4i ⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝐴 )