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