Theorem bnj985

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). See bnj985v for a version with more disjoint variable conditions, not requiring ax-13 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj985.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
	bnj985.6	|- ( ch' <-> [. p / n ]. ch )
	bnj985.9	|- ( ch" <-> [. G / f ]. ch' )
	bnj985.11	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
	bnj985.13	|- G = ( f u. { <. n , C >. } )
Assertion	bnj985	|- ( G e. B <-> E. p ch" )

Proof

Step	Hyp	Ref	Expression
1		bnj985.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2		bnj985.6	|- ( ch' <-> [. p / n ]. ch )
3		bnj985.9	|- ( ch" <-> [. G / f ]. ch' )
4		bnj985.11	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5		bnj985.13	|- G = ( f u. { <. n , C >. } )
6	5	bnj918	|- G e. _V
7	1 4	bnj984	|- ( G e. _V -> ( G e. B <-> [. G / f ]. E. n ch ) )
8	6 7	ax-mp	|- ( G e. B <-> [. G / f ]. E. n ch )
9		sbcex2	|- ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' )
10		nfv	|- F/ p ch
11	10	sb8e	|- ( E. n ch <-> E. p [ p / n ] ch )
12		sbsbc	|- ( [ p / n ] ch <-> [. p / n ]. ch )
13	12	exbii	|- ( E. p [ p / n ] ch <-> E. p [. p / n ]. ch )
14	11 13	bitri	|- ( E. n ch <-> E. p [. p / n ]. ch )
15	14 2	bnj133	|- ( E. n ch <-> E. p ch' )
16	15	sbcbii	|- ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' )
17	3	exbii	|- ( E. p ch" <-> E. p [. G / f ]. ch' )
18	9 16 17	3bitr4i	|- ( [. G / f ]. E. n ch <-> E. p ch" )
19	8 18	bitri	|- ( G e. B <-> E. p ch" )