Theorem csbprc 4410

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 3788	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1550	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 376	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2797	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3895	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1547	. . . 4 ⊢ ¬ ⊥
7	6	abf 4406	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2737	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2793	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533  ⊥wfal 1545   ∈ wcel 2098  {cab 2705  Vcvv 3473  [wsbc 3778  ⦋csb 3894  ∅c0 4326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-nul 4327

This theorem is referenced by:  csb0  4411  sbcel12  4412  sbcne12  4416  sbcel2  4419  csbidm  4434  csbun  4442  csbin  4443  csbdif  4531  csbif  4589  csbuni  4943  sbcbr123  5206  sbcbr  5207  csbexg  5314  csbopab  5561  csbxp  5781  csbres  5992  csbima12  6087  csbrn  6212  csbiota  6546  csbfv12  6950  csbfv  6952  csbriota  7398  csbov123  7468  csbov  7469