Theorem substitution ≪ | index | src | ≫

替换公理

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

Step	Hyp	Ref	Expression
1		ax_12	x = y \imp P \imp \fo x (x = y \imp P)

Axiom use

Logic (ax_12)