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	⊢ ( 𝜂 ↔ ∀ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )