Theorem hashrabsn1

Description: If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018)

	Ref	Expression
Assertion	hashrabsn1	$$⊢\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\left\{x\in \left\{A\right\}|\phi \right\}$$
2		rabrsn	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\left\{x\in \left\{A\right\}|\phi \right\}\to \left(\left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \vee \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)$$
3		fveqeq2	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\leftrightarrow \left|\varnothing \right|=1\right)$$
4		hash0	$$⊢\left|\varnothing \right|=0$$
5	4	eqeq1i	$$⊢\left|\varnothing \right|=1\leftrightarrow 0=1$$
6		0ne1	$$⊢0\ne 1$$
7		eqneqall	$$⊢0=1\to \left(0\ne 1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
8	6 7	mpi	$$⊢0=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
9	5 8	sylbi	$$⊢\left|\varnothing \right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
10	3 9	syl6bi	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
11		snidg	$$⊢A\in \mathrm{V}\to A\in \left\{A\right\}$$
12	11	adantr	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to A\in \left\{A\right\}$$
13		eleq2	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\to \left(A\in \left\{x\in \left\{A\right\}|\phi \right\}\leftrightarrow A\in \left\{A\right\}\right)$$
14	13	adantl	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to \left(A\in \left\{x\in \left\{A\right\}|\phi \right\}\leftrightarrow A\in \left\{A\right\}\right)$$
15	12 14	mpbird	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to A\in \left\{x\in \left\{A\right\}|\phi \right\}$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}$$
17	16	elrabsf	$$⊢A\in \left\{x\in \left\{A\right\}|\phi \right\}\leftrightarrow \left(A\in \left\{A\right\}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
18	17	simprbi	$$⊢A\in \left\{x\in \left\{A\right\}|\phi \right\}\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
19	15 18	syl	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
20	19	a1d	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
21	20	ex	$$⊢A\in \mathrm{V}\to \left(\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
22		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
23		eqeq2	$$⊢\left\{A\right\}=\varnothing \to \left(\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\leftrightarrow \left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \right)$$
24		ax-1ne0	$$⊢1\ne 0$$
25		eqneqall	$$⊢1=0\to \left(1\ne 0\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
26	24 25	mpi	$$⊢1=0\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
27	26	eqcoms	$$⊢0=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
28	5 27	sylbi	$$⊢\left|\varnothing \right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
29	3 28	syl6bi	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
30	23 29	syl6bi	$$⊢\left\{A\right\}=\varnothing \to \left(\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
31	22 30	sylbi	$$⊢\neg A\in \mathrm{V}\to \left(\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
32	21 31	pm2.61i	$$⊢\left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
33	10 32	jaoi	$$⊢\left(\left\{x\in \left\{A\right\}|\phi \right\}=\varnothing \vee \left\{x\in \left\{A\right\}|\phi \right\}=\left\{A\right\}\right)\to \left(\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
34	1 2 33	mp2b	$$⊢\left|\left\{x\in \left\{A\right\}|\phi \right\}\right|=1\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$