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 2829	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3852	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		dfnul4 4283	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
7	4, 5, 6	3eqtr4g 2823	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ⊥wfal 1582   ∈ wcel 2147  {cab 2741  Vcvv 3454  [wsbc 3742  ⦋csb 3851  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sbc 3743  df-csb 3852  df-dif 4050  df-nul 4282

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  5267  csbopab  5534  csbxp  5757  csbcnv  5871  csbres  5984  csbima12  6088  csbrn  6217  csbiota  6551  csbfv12  6953  csbfv  6955  csbriota  7415  csbov123  7487  csbov  7488  csbttc  37475