Theorem dfafn5b

Description: Representation of a function in terms of its values, analogous to dffn5 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	dfafn5b	$$⊢\forall x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\in V\to \left(FFnA\leftrightarrow F=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfafn5a	$$⊢FFnA\to F=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)$$
2		eqid	$$⊢\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)$$
3	2	fnmpt	$$⊢\forall x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\in V\to \left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)FnA$$
4		fneq1	$$⊢F=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)\to \left(FFnA\leftrightarrow \left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)FnA\right)$$
5	3 4	syl5ibrcom	$$⊢\forall x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\in V\to \left(F=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)\to FFnA\right)$$
6	1 5	impbid2	$$⊢\forall x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\in V\to \left(FFnA\leftrightarrow F=\left(x\in A⟼\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)\right)$$