Theorem rabsnif

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

	Ref	Expression
Hypothesis	rabsnif.f	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rabsnif	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\psi ,\left\{A\right\},\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		rabsnif.f	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		rabsnifsb	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)$$
3	1	sbcieg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
4	3	ifbid	$$⊢A\in \mathrm{V}\to if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=if\left(\psi ,\left\{A\right\},\varnothing \right)$$
5	2 4	syl5eq	$$⊢A\in \mathrm{V}\to \left\{x\in \left\{A\right\}|\phi \right\}=if\left(\psi ,\left\{A\right\},\varnothing \right)$$
6		rab0	$$⊢\left\{x\in \varnothing |\phi \right\}=\varnothing$$
7		ifid	$$⊢if\left(\psi ,\varnothing ,\varnothing \right)=\varnothing$$
8	6 7	eqtr4i	$$⊢\left\{x\in \varnothing |\phi \right\}=if\left(\psi ,\varnothing ,\varnothing \right)$$
9		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
10	9	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
11	10	rabeqdv	$$⊢\neg A\in \mathrm{V}\to \left\{x\in \left\{A\right\}|\phi \right\}=\left\{x\in \varnothing |\phi \right\}$$
12	10	ifeq1d	$$⊢\neg A\in \mathrm{V}\to if\left(\psi ,\left\{A\right\},\varnothing \right)=if\left(\psi ,\varnothing ,\varnothing \right)$$
13	8 11 12	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to \left\{x\in \left\{A\right\}|\phi \right\}=if\left(\psi ,\left\{A\right\},\varnothing \right)$$
14	5 13	pm2.61i	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\psi ,\left\{A\right\},\varnothing \right)$$