Theorem csbprc 4370

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 3752	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1587	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 380	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2828	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3851	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		dfnul4 4284	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
7	4, 5, 6	3eqtr4g 2822	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ⊥wfal 1582   ∈ wcel 2145  {cab 2740  Vcvv 3453  [wsbc 3742  ⦋csb 3850  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-nul 4283

This theorem is used by:  csb0  4371  sbcel12  4372  sbcne12  4376  sbcel2  4379  csbidm  4394  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  csbuni  4901  sbcbr123  5163  sbcbr  5164  csbexg  5271  csbopab  5538  csbxp  5760  csbcnv  5870  csbres  5979  csbima12  6079  csbrn  6203  csbiota  6530  csbfv12  6927  csbfv  6929  csbriota  7388  csbov123  7460  csbov  7461  csbttc  37130