普通はZFC以前に述語論理で「=」が導入される
それが嫌ならそうしないでもいいけど
後で面倒になって後悔するよってだけ

「=」が明示的に使われていないZFCの公理でも
実は「=」つき述語論理の
substitution x = y ⇒ ( P(x) ⇔ P(y) )
を前提にしてるから