Metamath Proof Explorer


Theorem bnj1047

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 bnj1047.1
|- ( rh <-> A. j e. n ( j _E i -> [. j / i ]. et ) )
bnj1047.2
|- ( et' <-> [. j / i ]. et )
Assertion bnj1047
|- ( rh <-> A. j e. n ( j _E i -> et' ) )

Proof

Step Hyp Ref Expression
1 bnj1047.1
 |-  ( rh <-> A. j e. n ( j _E i -> [. j / i ]. et ) )
2 bnj1047.2
 |-  ( et' <-> [. j / i ]. et )
3 2 imbi2i
 |-  ( ( j _E i -> et' ) <-> ( j _E i -> [. j / i ]. et ) )
4 3 ralbii
 |-  ( A. j e. n ( j _E i -> et' ) <-> A. j e. n ( j _E i -> [. j / i ]. et ) )
5 1 4 bitr4i
 |-  ( rh <-> A. j e. n ( j _E i -> et' ) )