# Metamath Proof Explorer

## Theorem bnj1049

Description: Technical lemma for bnj69 . 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.)

Ref Expression
Hypotheses bnj1049.1 ${⊢}{\zeta }↔\left({i}\in {n}\wedge {z}\in {f}\left({i}\right)\right)$
bnj1049.2 ${⊢}{\eta }↔\left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)$
Assertion bnj1049 ${⊢}\forall {i}\in {n}\phantom{\rule{.4em}{0ex}}{\eta }↔\forall {i}\phantom{\rule{.4em}{0ex}}{\eta }$

### Proof

Step Hyp Ref Expression
1 bnj1049.1 ${⊢}{\zeta }↔\left({i}\in {n}\wedge {z}\in {f}\left({i}\right)\right)$
2 bnj1049.2 ${⊢}{\eta }↔\left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)$
3 df-ral ${⊢}\forall {i}\in {n}\phantom{\rule{.4em}{0ex}}{\eta }↔\forall {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {n}\to {\eta }\right)$
4 2 imbi2i ${⊢}\left({i}\in {n}\to {\eta }\right)↔\left({i}\in {n}\to \left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)\right)$
5 impexp ${⊢}\left(\left({i}\in {n}\wedge \left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\right)\to {z}\in {B}\right)↔\left({i}\in {n}\to \left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)\right)$
6 4 5 bitr4i ${⊢}\left({i}\in {n}\to {\eta }\right)↔\left(\left({i}\in {n}\wedge \left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\right)\to {z}\in {B}\right)$
7 1 simplbi ${⊢}{\zeta }\to {i}\in {n}$
8 7 bnj708 ${⊢}\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {i}\in {n}$
9 8 pm4.71ri ${⊢}\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)↔\left({i}\in {n}\wedge \left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\right)$
10 9 bicomi ${⊢}\left({i}\in {n}\wedge \left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\right)↔\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)$
11 10 imbi1i ${⊢}\left(\left({i}\in {n}\wedge \left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\right)\to {z}\in {B}\right)↔\left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)$
12 6 11 bitri ${⊢}\left({i}\in {n}\to {\eta }\right)↔\left(\left({\theta }\wedge {\tau }\wedge {\chi }\wedge {\zeta }\right)\to {z}\in {B}\right)$
13 12 2 bitr4i ${⊢}\left({i}\in {n}\to {\eta }\right)↔{\eta }$
14 13 albii ${⊢}\forall {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {n}\to {\eta }\right)↔\forall {i}\phantom{\rule{.4em}{0ex}}{\eta }$
15 3 14 bitri ${⊢}\forall {i}\in {n}\phantom{\rule{.4em}{0ex}}{\eta }↔\forall {i}\phantom{\rule{.4em}{0ex}}{\eta }$