Axiom ax_12 ≪ | index | src | ≫

axiom ax_12 {x: set} (y: set) (P: wff x):
  $ x = y \imp P \imp \fo x (x = y \imp P) $;