Theorem bnj958

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	bnj958.1	|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
	bnj958.2	|- G = ( f u. { <. n , C >. } )
Assertion	bnj958	|- ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) )

Proof

Step	Hyp	Ref	Expression
1		bnj958.1	|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
2		bnj958.2	|- G = ( f u. { <. n , C >. } )
3		nfcv	|- F/_ y f
4		nfcv	|- F/_ y n
5		nfiu1	|- F/_ y U_ y e. ( f ` m ) _pred ( y , A , R )
6	1 5	nfcxfr	|- F/_ y C
7	4 6	nfop	|- F/_ y <. n , C >.
8	7	nfsn	|- F/_ y { <. n , C >. }
9	3 8	nfun	|- F/_ y ( f u. { <. n , C >. } )
10	2 9	nfcxfr	|- F/_ y G
11		nfcv	|- F/_ y i
12	10 11	nffv	|- F/_ y ( G ` i )
13	12	nfeq1	|- F/ y ( G ` i ) = ( f ` i )
14	13	nf5ri	|- ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) )