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	⊢ Ⅎ 𝑥 𝐴
	nfaov.3	⊢ Ⅎ 𝑥 𝐹
	nfaov.4	⊢ Ⅎ 𝑥 𝐵
Assertion	nfaov	⊢ Ⅎ 𝑥 (( 𝐴 𝐹 𝐵 ))

Proof

Step	Hyp	Ref	Expression
1		nfaov.2	⊢ Ⅎ 𝑥 𝐴
2		nfaov.3	⊢ Ⅎ 𝑥 𝐹
3		nfaov.4	⊢ Ⅎ 𝑥 𝐵
4		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
5	1 3	nfop	⊢ Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩
6	2 5	nfafv	⊢ Ⅎ 𝑥 ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
7	4 6	nfcxfr	⊢ Ⅎ 𝑥 (( 𝐴 𝐹 𝐵 ))