Theorem bnj1049 35604

Description: Technical lemma for bnj69 35640. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj1049.1	⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
bnj1049.2	⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))

Assertion

Ref	Expression
bnj1049	⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖𝜂)

Proof of Theorem bnj1049

Step	Hyp	Ref	Expression
1		df-ral 3077	. 2 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖(𝑖 ∈ 𝑛 → 𝜂))
2		bnj1049.2	. . . . . . 7 ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
3	2	imbi2i 339	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
4		impexp 456	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
5	3, 4	bitr4i 281	. . . . 5 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵))
6		bnj1049.1	. . . . . . . . . 10 ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
7	6	simplbi 502	. . . . . . . . 9 ⊢ (𝜁 → 𝑖 ∈ 𝑛)
8	7	bnj708 35387	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑖 ∈ 𝑛)
9	8	pm4.71ri 570	. . . . . . 7 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ (𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)))
10	9	bicomi 227	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁))
11	10	imbi1i 352	. . . . 5 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
12	5, 11	bitri 278	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
13	12, 2	bitr4i 281	. . 3 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ 𝜂)
14	13	albii 1851	. 2 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → 𝜂) ↔ ∀𝑖𝜂)
15	1, 14	bitri 278	1 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖𝜂)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ∈ wcel 2144  ∀wral 3076  ‘cfv 6538   ∧ w-bnj17 35317

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077  df-bnj17 35318

This theorem is used by:  bnj1052  35605