Theorem bj-alequex

Description: A fol lemma. See alequexv for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-alequex	$$⊢\forall x\left(x=y\to \phi \right)\to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax6e	$$⊢\exists xx=y$$
2		exim	$$⊢\forall x\left(x=y\to \phi \right)\to \left(\exists xx=y\to \exists x\phi \right)$$
3	1 2	mpi	$$⊢\forall x\left(x=y\to \phi \right)\to \exists x\phi$$