Theorem dfafv23

Description: A definition of function value in terms of iota, analogous to dffv3 . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	dfafv23	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\left(\iota x|x\in F\left[\left\{A\right\}\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfatafv2iota	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\left(\iota x|AFx\right)$$
2		dfdfat2	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \exists !xAFx\right)$$
3	2	simplbi	$$⊢F\mathrm{defAt}A\to A\in \mathrm{dom}F$$
4		elimasng	$$⊢\left(A\in \mathrm{dom}F\wedge x\in \mathrm{V}\right)\to \left(x\in F\left[\left\{A\right\}\right]\leftrightarrow ⟨A,x⟩\in F\right)$$
5	3 4	sylan	$$⊢\left(F\mathrm{defAt}A\wedge x\in \mathrm{V}\right)\to \left(x\in F\left[\left\{A\right\}\right]\leftrightarrow ⟨A,x⟩\in F\right)$$
6		df-br	$$⊢AFx\leftrightarrow ⟨A,x⟩\in F$$
7	5 6	bitr4di	$$⊢\left(F\mathrm{defAt}A\wedge x\in \mathrm{V}\right)\to \left(x\in F\left[\left\{A\right\}\right]\leftrightarrow AFx\right)$$
8	7	elvd	$$⊢F\mathrm{defAt}A\to \left(x\in F\left[\left\{A\right\}\right]\leftrightarrow AFx\right)$$
9	8	iotabidv	$$⊢F\mathrm{defAt}A\to \left(\iota x|x\in F\left[\left\{A\right\}\right]\right)=\left(\iota x|AFx\right)$$
10	1 9	eqtr4d	$$⊢F\mathrm{defAt}A\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\left(\iota x|x\in F\left[\left\{A\right\}\right]\right)$$