Theorem csbprc 4362

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ⊥wfal 1552   ∈ wcel 2109  {cab 2707  Vcvv 3438  [wsbc 3744  ⦋csb 3853  ∅c0 4286

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-nul 4287

This theorem is referenced by:  csb0  4363  sbcel12  4364  sbcne12  4368  sbcel2  4371  csbidm  4386  csbun  4394  csbin  4395  csbdif  4477  csbif  4536  csbuni  4890  sbcbr123  5149  sbcbr  5150  csbexg  5252  csbopab  5502  csbxp  5723  csbres  5937  csbima12  6034  csbrn  6156  csbiota  6479  csbfv12  6872  csbfv  6874  csbriota  7325  csbov123  7397  csbov  7398