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 F = x A x
mptsnun.r R = u | x A u = x
Assertion mptsnun B A B = F B

Proof

Step Hyp Ref Expression
1 mptsnun.f F = x A x
2 mptsnun.r R = u | x A u = x
3 sneq x = y x = y
4 3 cbvmptv x A x = y A y
5 4 eqcomi y A y = x A x
6 5 2 mptsnunlem B A B = y A y B
7 1 4 eqtri F = y A y
8 7 imaeq1i F B = y A y B
9 8 unieqi F B = y A y B
10 6 9 eqtr4di B A B = F B