[STATEMENT]
lemma filter_single_zmset: "filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)
[PROOF STEP]
by (rule zmultiset_eqI) simp