Theorem axi9

Description: Axiom of existence (intuitionistic logic axiom ax-i9). In classical logic, this is equivalent to ax-6 but in intuitionistic logic it needs to be stated using the existential quantifier. (Contributed by Jim Kingdon, 31-Dec-2017) (New usage is discouraged.)

	Ref	Expression
Assertion	axi9	⊢ ∃ 𝑥 𝑥 = 𝑦

Proof

Step	Hyp	Ref	Expression
1		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦