像の存在

単なる像の存在と置換公理

• ∀f.∀A.∀B.( function(f, A, B)⇒( ∃C.∀y.( y∈C ⇔ ∃x∈A.(y = f(x)) ) ) )
• ∀F.( DefinableClassFunction(F)⇒∀A.( ∃C.∀y.( y∈C ⇔ ∃x∈A.(y = F(x)) ) ) )

太字の変数Fは、集合論の内部の実体を表す変数ではなくて、集合の宇宙の外にある構文的対応を走る変数。