Theorem csbprc 4340

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.)

Assertion

Ref	Expression
csbprc	⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Proof of Theorem csbprc

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbcex 3726	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1556	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 379	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2807	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3833	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1553	. . . 4 ⊢ ¬ ⊥
7	6	abf 4336	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2747	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2803	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539  ⊥wfal 1551   ∈ wcel 2106  {cab 2715  Vcvv 3432  [wsbc 3716  ⦋csb 3832  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-nul 4257

This theorem is referenced by:  csb0  4341  sbcel12  4342  sbcne12  4346  sbcel2  4349  csbidm  4364  csbun  4372  csbin  4373  csbdif  4458  csbif  4516  csbuni  4870  sbcbr123  5128  sbcbr  5129  csbexg  5234  csbopab  5468  csbxp  5686  csbres  5894  csbima12  5987  csbrn  6106  csbiota  6426  csbfv12  6817  csbfv  6819  csbriota  7248  csbov123  7317  csbov  7318