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 ρ j n j E i [˙j / i]˙ η
bnj1047.2 No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |-
Assertion bnj1047 Could not format assertion : No typesetting found for |- ( rh <-> A. j e. n ( j _E i -> et' ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj1047.1 ρ j n j E i [˙j / i]˙ η
2 bnj1047.2 Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |-
3 2 imbi2i Could not format ( ( j _E i -> et' ) <-> ( j _E i -> [. j / i ]. et ) ) : No typesetting found for |- ( ( j _E i -> et' ) <-> ( j _E i -> [. j / i ]. et ) ) with typecode |-
4 3 ralbii Could not format ( A. j e. n ( j _E i -> et' ) <-> A. j e. n ( j _E i -> [. j / i ]. et ) ) : No typesetting found for |- ( A. j e. n ( j _E i -> et' ) <-> A. j e. n ( j _E i -> [. j / i ]. et ) ) with typecode |-
5 1 4 bitr4i Could not format ( rh <-> A. j e. n ( j _E i -> et' ) ) : No typesetting found for |- ( rh <-> A. j e. n ( j _E i -> et' ) ) with typecode |-