This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 | 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 nfrexw 
 |-  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' ) }