Theorem nfco

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

	Ref	Expression
Hypotheses	nfco.1	⊢ Ⅎ 𝑥 𝐴
	nfco.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfco	⊢ Ⅎ 𝑥 ( 𝐴 ∘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfco.1	⊢ Ⅎ 𝑥 𝐴
2		nfco.2	⊢ Ⅎ 𝑥 𝐵
3		df-co	⊢ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) }
4		nfcv	⊢ Ⅎ 𝑥 𝑦
5		nfcv	⊢ Ⅎ 𝑥 𝑤
6	4 2 5	nfbr	⊢ Ⅎ 𝑥 𝑦 𝐵 𝑤
7		nfcv	⊢ Ⅎ 𝑥 𝑧
8	5 1 7	nfbr	⊢ Ⅎ 𝑥 𝑤 𝐴 𝑧
9	6 8	nfan	⊢ Ⅎ 𝑥 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 )
10	9	nfex	⊢ Ⅎ 𝑥 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 )
11	10	nfopab	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) }
12	3 11	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 ∘ 𝐵 )