# Metamath Proof Explorer

## 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 ) )`