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 = f | n D f Fn n φ ψ
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 = f | n D f Fn n φ ψ
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 n D f Fn n φ ψ
5 nfcv _ f D
6 nfv f g Fn n
7 nfsbc1v f [˙g / f]˙ φ
8 2 7 nfxfr Could not format F/ f ph' : No typesetting found for |- F/ f ph' with typecode |-
9 nfsbc1v f [˙g / f]˙ ψ
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 f Fn n g Fn n
14 sbceq1a f = g φ [˙g / f]˙ φ
15 14 2 bitr4di Could not format ( f = g -> ( ph <-> ph' ) ) : No typesetting found for |- ( f = g -> ( ph <-> ph' ) ) with typecode |-
16 sbceq1a f = g ψ [˙g / f]˙ ψ
17 16 3 bitr4di 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 |-