Theorem bnj1049 32241

Description: Technical lemma for bnj69 32277. 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 3143	. 2 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖(𝑖 ∈ 𝑛 → 𝜂))
2		bnj1049.2	. . . . . . 7 ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
3	2	imbi2i 338	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
4		impexp 453	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ (𝑖 ∈ 𝑛 → ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)))
5	3, 4	bitr4i 280	. . . . 5 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵))
6		bnj1049.1	. . . . . . . . . 10 ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
7	6	simplbi 500	. . . . . . . . 9 ⊢ (𝜁 → 𝑖 ∈ 𝑛)
8	7	bnj708 32022	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑖 ∈ 𝑛)
9	8	pm4.71ri 563	. . . . . . 7 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ (𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)))
10	9	bicomi 226	. . . . . 6 ⊢ ((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁))
11	10	imbi1i 352	. . . . 5 ⊢ (((𝑖 ∈ 𝑛 ∧ (𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁)) → 𝑧 ∈ 𝐵) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
12	5, 11	bitri 277	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
13	12, 2	bitr4i 280	. . 3 ⊢ ((𝑖 ∈ 𝑛 → 𝜂) ↔ 𝜂)
14	13	albii 1816	. 2 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → 𝜂) ↔ ∀𝑖𝜂)
15	1, 14	bitri 277	1 ⊢ (∀𝑖 ∈ 𝑛 𝜂 ↔ ∀𝑖𝜂)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531   ∈ wcel 2110  ∀wral 3138  ‘cfv 6349   ∧ w-bnj17 31951

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143  df-bnj17 31952

This theorem is referenced by:  bnj1052  32242