Theorem csbprc

Description: The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018) (Proof shortened by JJ, 27-Aug-2021)

	Ref	Expression
Assertion	csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\to A\in \mathrm{V}$$
2		falim	$$⊢\perp \to A\in \mathrm{V}$$
3	1 2	pm5.21ni	$$⊢\neg A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow \perp \right)$$
4	3	abbidv	$$⊢\neg A\in \mathrm{V}\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\perp \right\}$$
5		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
6		fal	$$⊢\neg \perp$$
7	6	abf	$$⊢\left\{y|\perp \right\}=\varnothing$$
8	7	eqcomi	$$⊢\varnothing =\left\{y|\perp \right\}$$
9	4 5 8	3eqtr4g	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$