Theorem rexsb

Description: An equivalent expression for restricted existence, analogous to exsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

	Ref	Expression
Assertion	rexsb	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in A\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	cbvrexw	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in A\forall x\left(x=y\to \phi \right)$$