Metamath Proof Explorer


Theorem mptsnun

Description: A class B is equal to the union of the class of all singletons of elements of B . (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypotheses mptsnun.f 𝐹 = ( 𝑥𝐴 ↦ { 𝑥 } )
mptsnun.r 𝑅 = { 𝑢 ∣ ∃ 𝑥𝐴 𝑢 = { 𝑥 } }
Assertion mptsnun ( 𝐵𝐴𝐵 = ( 𝐹𝐵 ) )

Proof

Step Hyp Ref Expression
1 mptsnun.f 𝐹 = ( 𝑥𝐴 ↦ { 𝑥 } )
2 mptsnun.r 𝑅 = { 𝑢 ∣ ∃ 𝑥𝐴 𝑢 = { 𝑥 } }
3 sneq ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
4 3 cbvmptv ( 𝑥𝐴 ↦ { 𝑥 } ) = ( 𝑦𝐴 ↦ { 𝑦 } )
5 4 eqcomi ( 𝑦𝐴 ↦ { 𝑦 } ) = ( 𝑥𝐴 ↦ { 𝑥 } )
6 5 2 mptsnunlem ( 𝐵𝐴𝐵 = ( ( 𝑦𝐴 ↦ { 𝑦 } ) “ 𝐵 ) )
7 1 4 eqtri 𝐹 = ( 𝑦𝐴 ↦ { 𝑦 } )
8 7 imaeq1i ( 𝐹𝐵 ) = ( ( 𝑦𝐴 ↦ { 𝑦 } ) “ 𝐵 )
9 8 unieqi ( 𝐹𝐵 ) = ( ( 𝑦𝐴 ↦ { 𝑦 } ) “ 𝐵 )
10 6 9 eqtr4di ( 𝐵𝐴𝐵 = ( 𝐹𝐵 ) )