Theorem csbprc 4337

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 3721	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1556	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 378	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2808	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3829	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1553	. . . 4 ⊢ ¬ ⊥
7	6	abf 4333	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2747	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2804	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539  ⊥wfal 1551   ∈ wcel 2108  {cab 2715  Vcvv 3422  [wsbc 3711  ⦋csb 3828  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-nul 4254

This theorem is referenced by:  csb0  4338  sbcel12  4339  sbcne12  4343  sbcel2  4346  csbidm  4361  csbun  4369  csbin  4370  csbdif  4455  csbif  4513  csbuni  4867  sbcbr123  5124  sbcbr  5125  csbexg  5229  csbopab  5461  csbxp  5676  csbres  5883  csbima12  5976  csbrn  6095  csbiota  6411  csbfv12  6799  csbfv  6801  csbriota  7228  csbov123  7297  csbov  7298