# Metamath Proof Explorer

## Theorem bnj873

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 bnj873.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
bnj873.7 No typesetting found for |- ( ph' <-> [. g / f ]. ph ) with typecode |-
bnj873.8 No typesetting found for |- ( ps' <-> [. g / f ]. ps ) with typecode |-
Assertion bnj873 Could not format assertion : No typesetting found for |- B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode |-

### Proof

Step Hyp Ref Expression
1 bnj873.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
2 bnj873.7 Could not format ( ph' <-> [. g / f ]. ph ) : No typesetting found for |- ( ph' <-> [. g / f ]. ph ) with typecode |-
3 bnj873.8 Could not format ( ps' <-> [. g / f ]. ps ) : No typesetting found for |- ( ps' <-> [. g / f ]. ps ) with typecode |-
4 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
5 nfcv ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{D}$
6 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{g}Fn{n}$
7 nfsbc1v
8 2 7 nfxfr Could not format F/ f ph' : No typesetting found for |- F/ f ph' with typecode |-
9 nfsbc1v
10 3 9 nfxfr Could not format F/ f ps' : No typesetting found for |- F/ f ps' with typecode |-
11 6 8 10 nf3an Could not format F/ f ( g Fn n /\ ph' /\ ps' ) : No typesetting found for |- F/ f ( g Fn n /\ ph' /\ ps' ) with typecode |-
12 5 11 nfrex Could not format F/ f E. n e. D ( g Fn n /\ ph' /\ ps' ) : No typesetting found for |- F/ f E. n e. D ( g Fn n /\ ph' /\ ps' ) with typecode |-
13 fneq1 ${⊢}{f}={g}\to \left({f}Fn{n}↔{g}Fn{n}\right)$
14 sbceq1a
15 14 2 syl6bbr Could not format ( f = g -> ( ph <-> ph' ) ) : No typesetting found for |- ( f = g -> ( ph <-> ph' ) ) with typecode |-
16 sbceq1a
17 16 3 syl6bbr Could not format ( f = g -> ( ps <-> ps' ) ) : No typesetting found for |- ( f = g -> ( ps <-> ps' ) ) with typecode |-
18 13 15 17 3anbi123d Could not format ( f = g -> ( ( f Fn n /\ ph /\ ps ) <-> ( g Fn n /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( f = g -> ( ( f Fn n /\ ph /\ ps ) <-> ( g Fn n /\ ph' /\ ps' ) ) ) with typecode |-
19 18 rexbidv Could not format ( f = g -> ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n e. D ( g Fn n /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( f = g -> ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n e. D ( g Fn n /\ ph' /\ ps' ) ) ) with typecode |-
20 4 12 19 cbvabw Could not format { f | E. n e. D ( f Fn n /\ ph /\ ps ) } = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } : No typesetting found for |- { f | E. n e. D ( f Fn n /\ ph /\ ps ) } = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode |-
21 1 20 eqtri Could not format B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } : No typesetting found for |- B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode |-