Theorem nfaov

Description: Bound-variable hypothesis builder for operation value, analogous to nfov . To prove a deduction version of this analogous to nfovd is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv ). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	nfaov.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nfaov.3	$$⊢\underset{\_}{Ⅎ}xF$$
	nfaov.4	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfaov	$$⊢\underset{\_}{Ⅎ}x((AFB))$$

Proof

Step	Hyp	Ref	Expression
1		nfaov.2	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfaov.3	$$⊢\underset{\_}{Ⅎ}xF$$
3		nfaov.4	$$⊢\underset{\_}{Ⅎ}xB$$
4		df-aov	$$⊢((AFB))=\left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)$$
5	1 3	nfop	$$⊢\underset{\_}{Ⅎ}x⟨A,B⟩$$
6	2 5	nfafv	$$⊢\underset{\_}{Ⅎ}x\left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)$$
7	4 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}x((AFB))$$