Axiom ax_e4 ≪ | index | src | ≫

axiom ax_e4 {x y: set} (P Q: wff x y):
  $ \fo x \fo y (x \eq y \and (\rep{y}{x} P \iff \rep{y}{x} Q) \imp (P \iff Q)
  ) $;