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	|- ( ze <-> ( i e. n /\ z e. ( f ` i ) ) )
	bnj1049.2	|- ( et <-> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) )
Assertion	bnj1049	|- ( A. i e. n et <-> A. i et )

Proof

Step	Hyp	Ref	Expression
1		bnj1049.1	|- ( ze <-> ( i e. n /\ z e. ( f ` i ) ) )
2		bnj1049.2	|- ( et <-> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) )
3		df-ral	|- ( A. i e. n et <-> A. i ( i e. n -> et ) )
4	2	imbi2i	|- ( ( i e. n -> et ) <-> ( i e. n -> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) )
5		impexp	|- ( ( ( i e. n /\ ( th /\ ta /\ ch /\ ze ) ) -> z e. B ) <-> ( i e. n -> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) ) )
6	4 5	bitr4i	|- ( ( i e. n -> et ) <-> ( ( i e. n /\ ( th /\ ta /\ ch /\ ze ) ) -> z e. B ) )
7	1	simplbi	|- ( ze -> i e. n )
8	7	bnj708	|- ( ( th /\ ta /\ ch /\ ze ) -> i e. n )
9	8	pm4.71ri	|- ( ( th /\ ta /\ ch /\ ze ) <-> ( i e. n /\ ( th /\ ta /\ ch /\ ze ) ) )
10	9	bicomi	|- ( ( i e. n /\ ( th /\ ta /\ ch /\ ze ) ) <-> ( th /\ ta /\ ch /\ ze ) )
11	10	imbi1i	|- ( ( ( i e. n /\ ( th /\ ta /\ ch /\ ze ) ) -> z e. B ) <-> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) )
12	6 11	bitri	|- ( ( i e. n -> et ) <-> ( ( th /\ ta /\ ch /\ ze ) -> z e. B ) )
13	12 2	bitr4i	|- ( ( i e. n -> et ) <-> et )
14	13	albii	|- ( A. i ( i e. n -> et ) <-> A. i et )
15	3 14	bitri	|- ( A. i e. n et <-> A. i et )