Metamath Proof Explorer


Theorem bnj115

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj115.1 ( 𝜂 ↔ ∀ 𝑛𝐷 ( 𝜏𝜃 ) )
Assertion bnj115 ( 𝜂 ↔ ∀ 𝑛 ( ( 𝑛𝐷𝜏 ) → 𝜃 ) )

Proof

Step Hyp Ref Expression
1 bnj115.1 ( 𝜂 ↔ ∀ 𝑛𝐷 ( 𝜏𝜃 ) )
2 df-ral ( ∀ 𝑛𝐷 ( 𝜏𝜃 ) ↔ ∀ 𝑛 ( 𝑛𝐷 → ( 𝜏𝜃 ) ) )
3 impexp ( ( ( 𝑛𝐷𝜏 ) → 𝜃 ) ↔ ( 𝑛𝐷 → ( 𝜏𝜃 ) ) )
4 3 bicomi ( ( 𝑛𝐷 → ( 𝜏𝜃 ) ) ↔ ( ( 𝑛𝐷𝜏 ) → 𝜃 ) )
5 4 albii ( ∀ 𝑛 ( 𝑛𝐷 → ( 𝜏𝜃 ) ) ↔ ∀ 𝑛 ( ( 𝑛𝐷𝜏 ) → 𝜃 ) )
6 1 2 5 3bitri ( 𝜂 ↔ ∀ 𝑛 ( ( 𝑛𝐷𝜏 ) → 𝜃 ) )