Theorem csbprc 4415

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537  ⊥wfal 1549   ∈ wcel 2106  {cab 2712  Vcvv 3478  [wsbc 3791  ⦋csb 3908  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-nul 4340

This theorem is referenced by:  csb0  4416  sbcel12  4417  sbcne12  4421  sbcel2  4424  csbidm  4439  csbun  4447  csbin  4448  csbdif  4530  csbif  4588  csbuni  4941  sbcbr123  5202  sbcbr  5203  csbexg  5316  csbopab  5565  csbxp  5788  csbres  6003  csbima12  6099  csbrn  6225  csbiota  6556  csbfv12  6955  csbfv  6957  csbriota  7403  csbov123  7475  csbov  7476