Theorem csbprc 4384

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 3775	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1557	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 377	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2801	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3875	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1554	. . . 4 ⊢ ¬ ⊥
7	6	abf 4381	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2744	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2795	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ⊥wfal 1552   ∈ wcel 2108  {cab 2713  Vcvv 3459  [wsbc 3765  ⦋csb 3874  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-nul 4309

This theorem is referenced by:  csb0  4385  sbcel12  4386  sbcne12  4390  sbcel2  4393  csbidm  4408  csbun  4416  csbin  4417  csbdif  4499  csbif  4558  csbuni  4912  sbcbr123  5173  sbcbr  5174  csbexg  5280  csbopab  5530  csbxp  5754  csbres  5969  csbima12  6066  csbrn  6192  csbiota  6524  csbfv12  6924  csbfv  6926  csbriota  7377  csbov123  7449  csbov  7450