Theorem rexrsb

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

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

Proof

Step	Hyp	Ref	Expression
1		rexsb	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in A\forall x\left(x=y\to \phi \right)$$
2		alral	$$⊢\forall x\left(x=y\to \phi \right)\to \forall x\in A\left(x=y\to \phi \right)$$
3		df-ral	$$⊢\forall x\in A\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x\in A\to \left(x=y\to \phi \right)\right)$$
4		19.27v	$$⊢\forall x\left(\left(x\in A\to \left(x=y\to \phi \right)\right)\wedge y\in A\right)\leftrightarrow \left(\forall x\left(x\in A\to \left(x=y\to \phi \right)\right)\wedge y\in A\right)$$
5		pm2.04	$$⊢\left(x\in A\to \left(x=y\to \phi \right)\right)\to \left(x=y\to \left(x\in A\to \phi \right)\right)$$
6		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
7	6	biimprd	$$⊢x=y\to \left(y\in A\to x\in A\right)$$
8	7	imim1d	$$⊢x=y\to \left(\left(x\in A\to \phi \right)\to \left(y\in A\to \phi \right)\right)$$
9	8	a2i	$$⊢\left(x=y\to \left(x\in A\to \phi \right)\right)\to \left(x=y\to \left(y\in A\to \phi \right)\right)$$
10		pm2.04	$$⊢\left(x=y\to \left(y\in A\to \phi \right)\right)\to \left(y\in A\to \left(x=y\to \phi \right)\right)$$
11	5 9 10	3syl	$$⊢\left(x\in A\to \left(x=y\to \phi \right)\right)\to \left(y\in A\to \left(x=y\to \phi \right)\right)$$
12	11	imp	$$⊢\left(\left(x\in A\to \left(x=y\to \phi \right)\right)\wedge y\in A\right)\to \left(x=y\to \phi \right)$$
13	12	alimi	$$⊢\forall x\left(\left(x\in A\to \left(x=y\to \phi \right)\right)\wedge y\in A\right)\to \forall x\left(x=y\to \phi \right)$$
14	4 13	sylbir	$$⊢\left(\forall x\left(x\in A\to \left(x=y\to \phi \right)\right)\wedge y\in A\right)\to \forall x\left(x=y\to \phi \right)$$
15	14	ex	$$⊢\forall x\left(x\in A\to \left(x=y\to \phi \right)\right)\to \left(y\in A\to \forall x\left(x=y\to \phi \right)\right)$$
16	3 15	sylbi	$$⊢\forall x\in A\left(x=y\to \phi \right)\to \left(y\in A\to \forall x\left(x=y\to \phi \right)\right)$$
17	16	com12	$$⊢y\in A\to \left(\forall x\in A\left(x=y\to \phi \right)\to \forall x\left(x=y\to \phi \right)\right)$$
18	2 17	impbid2	$$⊢y\in A\to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \forall x\in A\left(x=y\to \phi \right)\right)$$
19	18	rexbiia	$$⊢\exists y\in A\forall x\left(x=y\to \phi \right)\leftrightarrow \exists y\in A\forall x\in A\left(x=y\to \phi \right)$$
20	1 19	bitri	$$⊢\exists x\in A\phi \leftrightarrow \exists y\in A\forall x\in A\left(x=y\to \phi \right)$$