Theorem csbprc 4357

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ⊥wfal 1553   ∈ wcel 2110  {cab 2708  Vcvv 3434  [wsbc 3739  ⦋csb 3848  ∅c0 4281

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-nul 4282

This theorem is referenced by:  csb0  4358  sbcel12  4359  sbcne12  4363  sbcel2  4366  csbidm  4381  csbun  4389  csbin  4390  csbdif  4472  csbif  4531  csbuni  4886  sbcbr123  5143  sbcbr  5144  csbexg  5246  csbopab  5493  csbxp  5714  csbres  5928  csbima12  6025  csbrn  6147  csbiota  6470  csbfv12  6862  csbfv  6864  csbriota  7313  csbov123  7385  csbov  7386