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 | E. n e. D ( f Fn n /\ ph /\ ps ) }
	bnj873.7	|- ( ph' <-> [. g / f ]. ph )
	bnj873.8	|- ( ps' <-> [. g / f ]. ps )
Assertion	bnj873	|- B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) }

Proof

Step	Hyp	Ref	Expression
1		bnj873.4	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
2		bnj873.7	|- ( ph' <-> [. g / f ]. ph )
3		bnj873.8	|- ( ps' <-> [. g / f ]. ps )
4		nfv	|- F/ g E. n e. D ( f Fn n /\ ph /\ ps )
5		nfcv	|- F/_ f D
6		nfv	|- F/ f g Fn n
7		nfsbc1v	|- F/ f [. g / f ]. ph
8	2 7	nfxfr	|- F/ f ph'
9		nfsbc1v	|- F/ f [. g / f ]. ps
10	3 9	nfxfr	|- F/ f ps'
11	6 8 10	nf3an	|- F/ f ( g Fn n /\ ph' /\ ps' )
12	5 11	nfrex	|- F/ f E. n e. D ( g Fn n /\ ph' /\ ps' )
13		fneq1	|- ( f = g -> ( f Fn n <-> g Fn n ) )
14		sbceq1a	|- ( f = g -> ( ph <-> [. g / f ]. ph ) )
15	14 2	bitr4di	|- ( f = g -> ( ph <-> ph' ) )
16		sbceq1a	|- ( f = g -> ( ps <-> [. g / f ]. ps ) )
17	16 3	bitr4di	|- ( f = g -> ( ps <-> ps' ) )
18	13 15 17	3anbi123d	|- ( f = g -> ( ( f Fn n /\ ph /\ ps ) <-> ( g Fn n /\ ph' /\ ps' ) ) )
19	18	rexbidv	|- ( f = g -> ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> E. n e. D ( g Fn n /\ ph' /\ ps' ) ) )
20	4 12 19	cbvabw	|- { f | E. n e. D ( f Fn n /\ ph /\ ps ) } = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) }
21	1 20	eqtri	|- B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) }