Theorem exsb

Description: An equivalent expression for existence. One direction ( exsbim ) needs fewer axioms. (Contributed by NM, 2-Feb-2005) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)

	Ref	Expression
Assertion	exsb	$$⊢\exists x\phi \leftrightarrow \exists y\forall x\left(x=y\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎy\phi$$
2		nfa1	$$⊢Ⅎx\forall x\left(x=y\to \phi \right)$$
3		ax12v	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
4		sp	$$⊢\forall x\left(x=y\to \phi \right)\to \left(x=y\to \phi \right)$$
5	4	com12	$$⊢x=y\to \left(\forall x\left(x=y\to \phi \right)\to \phi \right)$$
6	3 5	impbid	$$⊢x=y\to \left(\phi \leftrightarrow \forall x\left(x=y\to \phi \right)\right)$$
7	1 2 6	cbvexv1	$$⊢\exists x\phi \leftrightarrow \exists y\forall x\left(x=y\to \phi \right)$$