This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )