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 | ⊢ ( 𝜂 ↔ ∀ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj115.1 | ⊢ ( 𝜂 ↔ ∀ 𝑛 ∈ 𝐷 ( 𝜏 → 𝜃 ) ) | |
2 | df-ral | ⊢ ( ∀ 𝑛 ∈ 𝐷 ( 𝜏 → 𝜃 ) ↔ ∀ 𝑛 ( 𝑛 ∈ 𝐷 → ( 𝜏 → 𝜃 ) ) ) | |
3 | impexp | ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) ↔ ( 𝑛 ∈ 𝐷 → ( 𝜏 → 𝜃 ) ) ) | |
4 | 3 | bicomi | ⊢ ( ( 𝑛 ∈ 𝐷 → ( 𝜏 → 𝜃 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) ) |
5 | 4 | albii | ⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝐷 → ( 𝜏 → 𝜃 ) ) ↔ ∀ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) ) |
6 | 1 2 5 | 3bitri | ⊢ ( 𝜂 ↔ ∀ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) ) |