Theorem csb0 4314

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

Assertion

Ref	Expression
csb0	⊢ ⦋𝐴 / 𝑥⦌∅ = ∅

Proof of Theorem csb0

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  Ⅎwnf 1785  [wsb 2069   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  Vcvv 3441  [wsbc 3720  ⦋csb 3828  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-nul 4244

This theorem is referenced by:  disjdsct  30462  onfrALTlem5  41248  onfrALTlem4  41249  onfrALTlem5VD  41591  onfrALTlem4VD  41592