Theorem rabrsn

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Assertion	rabrsn	$$⊢M=\left\{x\in \left\{A\right\}|\phi \right\}\to \left(M=\varnothing \vee M=\left\{A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rabsnifsb	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)$$
2	1	eqeq2i	$$⊢M=\left\{x\in \left\{A\right\}|\phi \right\}\leftrightarrow M=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)$$
3		ifeqor	$$⊢\left(if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\vee if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \right)$$
4		orcom	$$⊢\left(if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\vee if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \right)\leftrightarrow \left(if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \vee if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\right)$$
5	3 4	mpbi	$$⊢\left(if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \vee if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\right)$$
6		eqeq1	$$⊢M=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)\to \left(M=\varnothing \leftrightarrow if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \right)$$
7		eqeq1	$$⊢M=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)\to \left(M=\left\{A\right\}\leftrightarrow if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\right)$$
8	6 7	orbi12d	$$⊢M=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)\to \left(\left(M=\varnothing \vee M=\left\{A\right\}\right)\leftrightarrow \left(if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\varnothing \vee if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)=\left\{A\right\}\right)\right)$$
9	5 8	mpbiri	$$⊢M=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\left\{A\right\},\varnothing \right)\to \left(M=\varnothing \vee M=\left\{A\right\}\right)$$
10	2 9	sylbi	$$⊢M=\left\{x\in \left\{A\right\}|\phi \right\}\to \left(M=\varnothing \vee M=\left\{A\right\}\right)$$