I figured out the symbolization, but I am unable to prove it since my professor does not let us use the EI (existential instantiation) rule. I can see that I have use the =E (substitution) rule if I have...
x = b, Bxc.
But I am not sure on how to get Bxc from the existential quantifier without having to use EI.
Ib ∧ Wb ∧ ∀x((Ix ∧ Wx) → x = b) , ∃x(Ix ∧ Wx ∧ Bxc ∧ ∀y((Wy ∧ Byc) → x = y)) ⊢ Bbc