Theorem nfco

Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999)

	Ref	Expression
Hypotheses	nfco.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfco.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfco	$$⊢\underset{\_}{Ⅎ}x\left(A\circ B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfco.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfco.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-co	$$⊢A\circ B=\left\{⟨y,z⟩|\exists w\left(yBw\wedge wAz\right)\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
6	4 2 5	nfbr	$$⊢ℲxyBw$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
8	5 1 7	nfbr	$$⊢ℲxwAz$$
9	6 8	nfan	$$⊢Ⅎx\left(yBw\wedge wAz\right)$$
10	9	nfex	$$⊢Ⅎx\exists w\left(yBw\wedge wAz\right)$$
11	10	nfopab	$$⊢\underset{\_}{Ⅎ}x\left\{⟨y,z⟩|\exists w\left(yBw\wedge wAz\right)\right\}$$
12	3 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(A\circ B\right)$$