Theorem csbprc 4360

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 3748	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1558	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 377	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2799	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3848	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1555	. . . 4 ⊢ ¬ ⊥
7	6	abf 4357	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2742	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2793	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ⊥wfal 1553   ∈ wcel 2113  {cab 2711  Vcvv 3438  [wsbc 3738  ⦋csb 3847  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-nul 4285

This theorem is referenced by:  csb0  4361  sbcel12  4362  sbcne12  4366  sbcel2  4369  csbidm  4384  csbun  4392  csbin  4393  csbdif  4475  csbif  4534  csbuni  4890  sbcbr123  5149  sbcbr  5150  csbexg  5252  csbopab  5500  csbxp  5722  csbres  5938  csbima12  6035  csbrn  6158  csbiota  6482  csbfv12  6876  csbfv  6878  csbriota  7327  csbov123  7399  csbov  7400