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 ⊢ η ↔ ∀ n ∈ D τ → θ
Assertion bnj115 ⊢ η ↔ ∀ n n ∈ D ∧ τ → θ

Proof

Step Hyp Ref Expression
1 bnj115.1 ⊢ η ↔ ∀ n ∈ D τ → θ
2 df-ral ⊢ ∀ n ∈ D τ → θ ↔ ∀ n n ∈ D → τ → θ
3 impexp ⊢ n ∈ D ∧ τ → θ ↔ n ∈ D → τ → θ
4 3 bicomi ⊢ n ∈ D → τ → θ ↔ n ∈ D ∧ τ → θ
5 4 albii ⊢ ∀ n n ∈ D → τ → θ ↔ ∀ n n ∈ D ∧ τ → θ
6 1 2 5 3bitri ⊢ η ↔ ∀ n n ∈ D ∧ τ → θ