zf에서 무한공리와 치환공리꼴로 공집합 공리를 유도할 수 있음

근데 치환공리꼴을 안 쓰고도 무한 공리만 써서 증명할 수 있는 거 아님?

일반적으로 쓰는 무한 공리는 다음 꼴인데

∃S(∃o[o∈S∧¬∃y(y∈o)]∧∀x∈S∃y∈S(∀z(z∈y⟺z∈x∨z=x)))

다음과 같이 공집합 공리를 유도할 수 있음

∃o[o∈S∧¬∃y(y∈o)]∧∀x∈S∃y∈S(∀z(z∈y⟺z∈x∨z=x))
∃o[o∈S∧¬∃y(y∈o)]
∃o(o∈S)∧∃o¬∃y(y∈o)
∃o¬∃y(y∈o)

유일성이 문제가 될 수도 있지만 외연 공리와 공집합 정의 때문에 자명하게 유일함

근데 언급하는 책이 없는 거 보면 뭔가 잘못됐나?