Theorem csbprc 4372

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 3763	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1557	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 377	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2795	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3863	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1554	. . . 4 ⊢ ¬ ⊥
7	6	abf 4369	. . 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 3447  [wsbc 3753  ⦋csb 3862  ∅c0 4296

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 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-nul 4297

This theorem is referenced by:  csb0  4373  sbcel12  4374  sbcne12  4378  sbcel2  4381  csbidm  4396  csbun  4404  csbin  4405  csbdif  4487  csbif  4546  csbuni  4900  sbcbr123  5161  sbcbr  5162  csbexg  5265  csbopab  5515  csbxp  5738  csbres  5953  csbima12  6050  csbrn  6176  csbiota  6504  csbfv12  6906  csbfv  6908  csbriota  7359  csbov123  7431  csbov  7432