Metamath Proof Explorer


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 )