Theorem dfafv22

Description: Alternate definition of ( F '''' A ) using ( FA ) directly. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	dfafv22	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,F\left(A\right),𝒫\bigcup \mathrm{ran}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-afv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$
2		df-fv	$$⊢F\left(A\right)=\left(\iota x|AFx\right)$$
3	2	eqcomi	$$⊢\left(\iota x|AFx\right)=F\left(A\right)$$
4		ifeq1	$$⊢\left(\iota x|AFx\right)=F\left(A\right)\to if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)=if\left(F\mathrm{defAt}A,F\left(A\right),𝒫\bigcup \mathrm{ran}F\right)$$
5	3 4	ax-mp	$$⊢if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)=if\left(F\mathrm{defAt}A,F\left(A\right),𝒫\bigcup \mathrm{ran}F\right)$$
6	1 5	eqtri	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,F\left(A\right),𝒫\bigcup \mathrm{ran}F\right)$$