Theorem bnj1307

Description: Technical lemma for bnj60 . 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	bnj1307.1	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
	bnj1307.2	$$⊢w\in B\to \forall xw\in B$$
Assertion	bnj1307	$$⊢w\in C\to \forall xw\in C$$

Proof

Step	Hyp	Ref	Expression
1		bnj1307.1	$$⊢C=\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
2		bnj1307.2	$$⊢w\in B\to \forall xw\in B$$
3	2	nfcii	$$⊢\underset{\_}{Ⅎ}xB$$
4		nfv	$$⊢ℲxfFnd$$
5		nfra1	$$⊢Ⅎx\forall x\in df\left(x\right)=G\left(Y\right)$$
6	4 5	nfan	$$⊢Ⅎx\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)$$
7	3 6	nfrex	$$⊢Ⅎx\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{f|\exists d\in B\left(fFnd\wedge \forall x\in df\left(x\right)=G\left(Y\right)\right)\right\}$$
9	1 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}xC$$
10	9	nfcrii	$$⊢w\in C\to \forall xw\in C$$