Theorem nfovd

Description: Deduction version of bound-variable hypothesis builder nfov . (Contributed by NM, 13-Dec-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	nfovd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfovd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xF$$
	nfovd.4	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfovd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(AFB\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfovd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfovd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xF$$
3		nfovd.4	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
4		df-ov	$$⊢AFB=F\left(⟨A,B⟩\right)$$
5	1 3	nfopd	$$⊢\phi \to \underset{\_}{Ⅎ}x⟨A,B⟩$$
6	2 5	nffvd	$$⊢\phi \to \underset{\_}{Ⅎ}xF\left(⟨A,B⟩\right)$$
7	4 6	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(AFB\right)$$