Theorem nfco

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

	Ref	Expression
Hypotheses	nfco.1	|- F/_ x A
	nfco.2	|- F/_ x B
Assertion	nfco	|- F/_ x ( A o. B )

Proof

Step	Hyp	Ref	Expression
1		nfco.1	|- F/_ x A
2		nfco.2	|- F/_ x B
3		df-co	|- ( A o. B ) = { <. y , z >. | E. w ( y B w /\ w A z ) }
4		nfcv	|- F/_ x y
5		nfcv	|- F/_ x w
6	4 2 5	nfbr	|- F/ x y B w
7		nfcv	|- F/_ x z
8	5 1 7	nfbr	|- F/ x w A z
9	6 8	nfan	|- F/ x ( y B w /\ w A z )
10	9	nfex	|- F/ x E. w ( y B w /\ w A z )
11	10	nfopab	|- F/_ x { <. y , z >. | E. w ( y B w /\ w A z ) }
12	3 11	nfcxfr	|- F/_ x ( A o. B )