Theorem csb0

Description: The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018)

	Ref	Expression
Assertion	csb0	$$⊢⦋A/x⦌\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\varnothing =\varnothing$$
2		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\varnothing =\varnothing$$
3	1 2	pm2.61i	$$⊢⦋A/x⦌\varnothing =\varnothing$$