Theorem dffv5

Description: Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	dffv5	$$⊢F\left(A\right)=\bigcup \bigcup \left(\left\{F\left[\left\{A\right\}\right]\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffv3	$$⊢F\left(A\right)=\left(\iota x|x\in F\left[\left\{A\right\}\right]\right)$$
2		dfiota3	$$⊢\left(\iota x|x\in F\left[\left\{A\right\}\right]\right)=\bigcup \bigcup \left(\left\{\left\{x|x\in F\left[\left\{A\right\}\right]\right\}\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$
3		abid2	$$⊢\left\{x|x\in F\left[\left\{A\right\}\right]\right\}=F\left[\left\{A\right\}\right]$$
4	3	sneqi	$$⊢\left\{\left\{x|x\in F\left[\left\{A\right\}\right]\right\}\right\}=\left\{F\left[\left\{A\right\}\right]\right\}$$
5	4	ineq1i	$$⊢\left\{\left\{x|x\in F\left[\left\{A\right\}\right]\right\}\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}=\left\{F\left[\left\{A\right\}\right]\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}$$
6	5	unieqi	$$⊢\bigcup \left(\left\{\left\{x|x\in F\left[\left\{A\right\}\right]\right\}\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)=\bigcup \left(\left\{F\left[\left\{A\right\}\right]\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$
7	6	unieqi	$$⊢\bigcup \bigcup \left(\left\{\left\{x|x\in F\left[\left\{A\right\}\right]\right\}\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)=\bigcup \bigcup \left(\left\{F\left[\left\{A\right\}\right]\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$
8	1 2 7	3eqtri	$$⊢F\left(A\right)=\bigcup \bigcup \left(\left\{F\left[\left\{A\right\}\right]\right\}\cap \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$