Theorem rexreusng

Description: Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023)

	Ref	Expression
Assertion	rexreusng	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}\phi \leftrightarrow \exists !x\in \left\{A\right\}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A=A$$
2		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
3		nfv	$$⊢Ⅎy\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
4	2 3	nfan	$$⊢Ⅎy\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
5		nfv	$$⊢ℲyA=A$$
6	4 5	nfim	$$⊢Ⅎy\left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A=A\right)$$
7		sbceq1a	$$⊢y=A\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
8		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
9	7 8	anbi12d	$$⊢y=A\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
10		eqeq2	$$⊢y=A\to \left(A=y\leftrightarrow A=A\right)$$
11	9 10	imbi12d	$$⊢y=A\to \left(\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A=A\right)\right)$$
12	6 11	ralsngf	$$⊢A\in V\to \left(\forall y\in \left\{A\right\}\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A=A\right)\right)$$
13	1 12	mpbiri	$$⊢A\in V\to \forall y\in \left\{A\right\}\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}$$
15		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
16		nfs1v	$$⊢Ⅎx\left[y/x\right]\phi$$
17	15 16	nfan	$$⊢Ⅎx\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)$$
18		nfv	$$⊢ℲxA=y$$
19	17 18	nfim	$$⊢Ⅎx\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)$$
20	14 19	nfralw	$$⊢Ⅎx\forall y\in \left\{A\right\}\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)$$
21		sbceq1a	$$⊢x=A\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
22	21	anbi1d	$$⊢x=A\to \left(\left(\phi \wedge \left[y/x\right]\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\right)$$
23		eqeq1	$$⊢x=A\to \left(x=y\leftrightarrow A=y\right)$$
24	22 23	imbi12d	$$⊢x=A\to \left(\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)\right)$$
25	24	ralbidv	$$⊢x=A\to \left(\forall y\in \left\{A\right\}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \forall y\in \left\{A\right\}\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)\right)$$
26	20 25	ralsngf	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\leftrightarrow \forall y\in \left\{A\right\}\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \left[y/x\right]\phi \right)\to A=y\right)\right)$$
27	13 26	mpbird	$$⊢A\in V\to \forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
28	27	biantrud	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}\phi \leftrightarrow \left(\exists x\in \left\{A\right\}\phi \wedge \forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)\right)$$
29		reu2	$$⊢\exists !x\in \left\{A\right\}\phi \leftrightarrow \left(\exists x\in \left\{A\right\}\phi \wedge \forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)\right)$$
30	28 29	bitr4di	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}\phi \leftrightarrow \exists !x\in \left\{A\right\}\phi \right)$$