# 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}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
bnj958.2 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
Assertion bnj958 ${⊢}{G}\left({i}\right)={f}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)={f}\left({i}\right)$

### Proof

Step Hyp Ref Expression
1 bnj958.1 ${⊢}{C}=\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
2 bnj958.2 ${⊢}{G}={f}\cup \left\{⟨{n},{C}⟩\right\}$
3 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{f}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{n}$
5 nfiu1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcup _{{y}\in {f}\left({m}\right)}pred\left({y},{A},{R}\right)$
6 1 5 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
7 4 6 nfop ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}⟨{n},{C}⟩$
8 7 nfsn ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨{n},{C}⟩\right\}$
9 3 8 nfun ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({f}\cup \left\{⟨{n},{C}⟩\right\}\right)$
10 2 9 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{G}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{i}$
12 10 11 nffv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)$
13 12 nfeq1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)={f}\left({i}\right)$
14 13 nf5ri ${⊢}{G}\left({i}\right)={f}\left({i}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)={f}\left({i}\right)$