Theorem rabsnifsb

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019)

	Ref	Expression
Assertion	rabsnifsb	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
2		sbceq1a	$$⊢x=A\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	biimpd	$$⊢x=A\to \left(\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 3	syl	$$⊢x\in \left\{A\right\}\to \left(\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
5	4	imdistani	$$⊢\left(x\in \left\{A\right\}\wedge \phi \right)\to \left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
6	5	orcd	$$⊢\left(x\in \left\{A\right\}\wedge \phi \right)\to \left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
7	2	biimprd	$$⊢x=A\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \phi \right)$$
8	1 7	syl	$$⊢x\in \left\{A\right\}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \phi \right)$$
9	8	imdistani	$$⊢\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to \left(x\in \left\{A\right\}\wedge \phi \right)$$
10		noel	$$⊢\neg x\in \varnothing$$
11	10	pm2.21i	$$⊢x\in \varnothing \to \left(x\in \left\{A\right\}\wedge \phi \right)$$
12	11	adantr	$$⊢\left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to \left(x\in \left\{A\right\}\wedge \phi \right)$$
13	9 12	jaoi	$$⊢\left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\to \left(x\in \left\{A\right\}\wedge \phi \right)$$
14	6 13	impbii	$$⊢\left(x\in \left\{A\right\}\wedge \phi \right)\leftrightarrow \left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
15	14	abbii	$$⊢\left\{x|\left(x\in \left\{A\right\}\wedge \phi \right)\right\}=\left\{x|\left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right\}$$
16		nfv	$$⊢Ⅎy\left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
17		nfv	$$⊢Ⅎxy\in \left\{A\right\}$$
18		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
19	17 18	nfan	$$⊢Ⅎx\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
20		nfv	$$⊢Ⅎxy\in \varnothing$$
21	18	nfn	$$⊢Ⅎx\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
22	20 21	nfan	$$⊢Ⅎx\left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
23	19 22	nfor	$$⊢Ⅎx\left(\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
24		eleq1w	$$⊢x=y\to \left(x\in \left\{A\right\}\leftrightarrow y\in \left\{A\right\}\right)$$
25	24	anbi1d	$$⊢x=y\to \left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
26		eleq1w	$$⊢x=y\to \left(x\in \varnothing \leftrightarrow y\in \varnothing \right)$$
27	26	anbi1d	$$⊢x=y\to \left(\left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
28	25 27	orbi12d	$$⊢x=y\to \left(\left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
29	16 23 28	cbvabw	$$⊢\left\{x|\left(\left(x\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(x\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right\}=\left\{y|\left(\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right\}$$
30	15 29	eqtri	$$⊢\left\{x|\left(x\in \left\{A\right\}\wedge \phi \right)\right\}=\left\{y|\left(\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right\}$$
31		df-rab	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\left\{x|\left(x\in \left\{A\right\}\wedge \phi \right)\right\}$$
32		df-if	$$⊢if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{y|\left(\left(y\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\vee \left(y\in \varnothing \wedge \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right\}$$
33	30 31 32	3eqtr4i	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)$$