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	|- ( -. A e. _V -> [_ A / x ]_ B = (/) )

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / x ]. y e. B -> A e. _V )
2		falim	|- ( F. -> A e. _V )
3	1 2	pm5.21ni	|- ( -. A e. _V -> ( [. A / x ]. y e. B <-> F. ) )
4	3	abbidv	|- ( -. A e. _V -> { y | [. A / x ]. y e. B } = { y | F. } )
5		df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
6		fal	|- -. F.
7	6	abf	|- { y | F. } = (/)
8	7	eqcomi	|- (/) = { y | F. }
9	4 5 8	3eqtr4g	|- ( -. A e. _V -> [_ A / x ]_ B = (/) )