Theorem csb0

Description: The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018) Avoid ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

	Ref	Expression
Assertion	csb0	|- [_ A / x ]_ (/) = (/)

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ x (/)
2		df-csb	|- [_ A / x ]_ (/) = { y | [. A / x ]. y e. (/) }
3		dfsbcq2	|- ( z = A -> ( [ z / x ] y e. (/) <-> [. A / x ]. y e. (/) ) )
4	3	bibi1d	|- ( z = A -> ( ( [ z / x ] y e. (/) <-> y e. (/) ) <-> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) )
5	4	imbi2d	|- ( z = A -> ( ( F/ x y e. (/) -> ( [ z / x ] y e. (/) <-> y e. (/) ) ) <-> ( F/ x y e. (/) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) ) )
6		sbv	|- ( [ z / x ] y e. (/) <-> y e. (/) )
7	6	a1i	|- ( F/ x y e. (/) -> ( [ z / x ] y e. (/) <-> y e. (/) ) )
8	5 7	vtoclg	|- ( A e. _V -> ( F/ x y e. (/) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) ) )
9		nfcr	|- ( F/_ x (/) -> F/ x y e. (/) )
10	8 9	impel	|- ( ( A e. _V /\ F/_ x (/) ) -> ( [. A / x ]. y e. (/) <-> y e. (/) ) )
11	10	abbi1dv	|- ( ( A e. _V /\ F/_ x (/) ) -> { y | [. A / x ]. y e. (/) } = (/) )
12	2 11	syl5eq	|- ( ( A e. _V /\ F/_ x (/) ) -> [_ A / x ]_ (/) = (/) )
13	1 12	mpan2	|- ( A e. _V -> [_ A / x ]_ (/) = (/) )
14		csbprc	|- ( -. A e. _V -> [_ A / x ]_ (/) = (/) )
15	13 14	pm2.61i	|- [_ A / x ]_ (/) = (/)