This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )