Theorem bnj1049 32854

Description: Technical lemma for bnj69 32890. 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 3068	. 2 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖(𝑖 ∈ 𝑛 → 𝜂))
2		bnj1049.2	. . . . . . 7 ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
3	2	imbi2i 335	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
4		impexp 450	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
5	3, 4	bitr4i 277	. . . . 5 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵))
6		bnj1049.1	. . . . . . . . . 10 ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
7	6	simplbi 497	. . . . . . . . 9 ⊢ (𝜁 → 𝑖 ∈ 𝑛)
8	7	bnj708 32636	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑖 ∈ 𝑛)
9	8	pm4.71ri 560	. . . . . . 7 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ (𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)))
10	9	bicomi 223	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁))
11	10	imbi1i 349	. . . . 5 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
12	5, 11	bitri 274	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
13	12, 2	bitr4i 277	. . 3 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ 𝜂)
14	13	albii 1823	. 2 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → 𝜂) ↔ ∀𝑖𝜂)
15	1, 14	bitri 274	1 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖𝜂)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   ∈ wcel 2108  ∀wral 3063  ‘cfv 6418   ∧ w-bnj17 32565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068  df-bnj17 32566

This theorem is referenced by:  bnj1052  32855