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	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑥 ∅
2		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∅ = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ }
3		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ∅ ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ ) )
4	3	bibi1d	⊢ ( 𝑧 = 𝐴 → ( ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) ) )
5	4	imbi2d	⊢ ( 𝑧 = 𝐴 → ( ( Ⅎ 𝑥 𝑦 ∈ ∅ → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) ) ↔ ( Ⅎ 𝑥 𝑦 ∈ ∅ → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) ) ) )
6		sbv	⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ )
7	6	a1i	⊢ ( Ⅎ 𝑥 𝑦 ∈ ∅ → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) )
8	5 7	vtoclg	⊢ ( 𝐴 ∈ V → ( Ⅎ 𝑥 𝑦 ∈ ∅ → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) ) )
9		nfcr	⊢ ( Ⅎ 𝑥 ∅ → Ⅎ 𝑥 𝑦 ∈ ∅ )
10	8 9	impel	⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑥 ∅ ) → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ ↔ 𝑦 ∈ ∅ ) )
11	10	abbi1dv	⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑥 ∅ ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ ∅ } = ∅ )
12	2 11	syl5eq	⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑥 ∅ ) → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
13	1 12	mpan2	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
14		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
15	13 14	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅