dffv5

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

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

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

Metamath Proof Explorer