Theorem bj-csbprc

Description: More direct proof of csbprc (fewer essential steps). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
2		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\to A\in \mathrm{V}$$
3	2	con3i	$$⊢\neg A\in \mathrm{V}\to \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B$$
4	3	alrimiv	$$⊢\neg A\in \mathrm{V}\to \forall y\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B$$
5		bj-ab0	$$⊢\forall y\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\varnothing$$
6	4 5	syl	$$⊢\neg A\in \mathrm{V}\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\varnothing$$
7	1 6	syl5eq	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$