Theorem dffv5

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

	Ref	Expression
Assertion	dffv5	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons )

Proof

Step	Hyp	Ref	Expression
1		dffv3	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) )
2		dfiota3	⊢ ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ∪ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons )
3		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } = ( 𝐹 “ { 𝐴 } )
4	3	sneqi	⊢ { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } = { ( 𝐹 “ { 𝐴 } ) }
5	4	ineq1i	⊢ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons )
6	5	unieqi	⊢ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons )
7	6	unieqi	⊢ ∪ ∪ ( { { 𝑥 ∣ 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) } } ∩ Singletons ) = ∪ ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons )
8	1 2 7	3eqtri	⊢ ( 𝐹 ‘ 𝐴 ) = ∪ ∪ ( { ( 𝐹 “ { 𝐴 } ) } ∩ Singletons )