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\left(fFnn\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\left(fFnn\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\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}fD$$
6		nfv	$$⊢ℲfgFnn$$
7		nfsbc1v	$$⊢Ⅎf\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\phi$$
8	2 7	nfxfr	Could not format F/ f ph' : No typesetting found for |- F/ f ph' with typecode |-
9		nfsbc1v	$$⊢Ⅎf\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\psi$$
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(fFnn\leftrightarrow gFnn\right)$$
14		sbceq1a	$$⊢f=g\to \left(\phi \leftrightarrow \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\phi \right)$$
15	14 2	syl6bbr	Could not format ( f = g -> ( ph <-> ph' ) ) : No typesetting found for |- ( f = g -> ( ph <-> ph' ) ) with typecode |-
16		sbceq1a	$$⊢f=g\to \left(\psi \leftrightarrow \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\psi \right)$$
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 |-