>>46
(u=x ∧ φ(u)) ⇒ φ(x) は使っていいのか?
とりあえず ⇒ の概略

上を使って
u=x∧t∈u ⇒ t∈x
u=x∧t∈u ⇒ t∈x∨t∈y　(∨導入)
u=x∧t∈u ⇒ ∃u(t∈x∨t∈y)　(∃導入)
同様に
u=y∧t∈u ⇒ ∃u(t∈x∨t∈y)
上2式に∨消去を使うと
(u=x∧t∈u)∨(u=y∧t∈u) ⇒ ∃u(t∈x∨t∈y)
((u=x∨u=y)∧t∈u) ⇒ ∃u(t∈x∨t∈y)
∃u((u=x∨u=y)∧t∈u) ⇒ ∃u(t∈x∨t∈y)　(∃消去)