Theorem absnsb

Description: If the class abstraction { x | ph } associated with the wff ph is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	absnsb	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
2		velsn	$$⊢x\in \left\{y\right\}\leftrightarrow x=y$$
3	1 2	bibi12i	$$⊢\left(x\in \left\{x|\phi \right\}\leftrightarrow x\in \left\{y\right\}\right)\leftrightarrow \left(\phi \leftrightarrow x=y\right)$$
4		biimpr	$$⊢\left(\phi \leftrightarrow x=y\right)\to \left(x=y\to \phi \right)$$
5	3 4	sylbi	$$⊢\left(x\in \left\{x|\phi \right\}\leftrightarrow x\in \left\{y\right\}\right)\to \left(x=y\to \phi \right)$$
6	5	alimi	$$⊢\forall x\left(x\in \left\{x|\phi \right\}\leftrightarrow x\in \left\{y\right\}\right)\to \forall x\left(x=y\to \phi \right)$$
7		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{y\right\}$$
9	7 8	cleqf	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \forall x\left(x\in \left\{x|\phi \right\}\leftrightarrow x\in \left\{y\right\}\right)$$
10		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
11	6 9 10	3imtr4i	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left[y/x\right]\phi$$