Theorem nfafv2

Description: Bound-variable hypothesis builder for function value, analogous to nffv . To prove a deduction version of this analogous to nffvd is not easily possible because a deduction version of nfdfat cannot be shown easily. (Contributed by AV, 4-Sep-2022)

	Ref	Expression
Hypotheses	nfafv2.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nfafv2.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfafv2	$$⊢\underset{\_}{Ⅎ}x\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfafv2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfafv2.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-afv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota y|AFy\right),𝒫\bigcup \mathrm{ran}F\right)$$
4	1 2	nfdfat	$$⊢ℲxF\mathrm{defAt}A$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
6	2 1 5	nfbr	$$⊢ℲxAFy$$
7	6	nfiotaw	$$⊢\underset{\_}{Ⅎ}x\left(\iota y|AFy\right)$$
8	1	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}F$$
9	8	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \mathrm{ran}F$$
10	9	nfpw	$$⊢\underset{\_}{Ⅎ}x𝒫\bigcup \mathrm{ran}F$$
11	4 7 10	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(F\mathrm{defAt}A,\left(\iota y|AFy\right),𝒫\bigcup \mathrm{ran}F\right)$$
12	3 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)$$