すいません。
またわからないことがあるのですが、
田中尚夫さんの「公理的集合論」で補題2.3.3で
「{ｘ、ｙ}＝{ｘ、ｚ}→ｙ＝ｚ」
を示すのに
ｙ＝ｘのときと¬(ｙ＝ｘ)のときで場合分けしてるのですが
「Ａ∨¬Ａ証明可能⇒Ａが証明可能またはＢが証明可能」が成立しないことを考えると
変じゃないですか？