Theorem csbprc 4366

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ⊥wfal 1582   ∈ wcel 2145  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846  ∅c0 4278

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-nul 4279

This theorem is used by:  csb0  4367  sbcel12  4368  sbcne12  4372  sbcel2  4375  csbidm  4390  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  csbuni  4897  sbcbr123  5158  sbcbr  5159  csbexg  5263  csbopab  5526  csbxp  5748  csbcnv  5860  csbres  5969  csbima12  6069  csbrn  6193  csbiota  6520  csbfv12  6918  csbfv  6920  csbriota  7380  csbov123  7452  csbov  7453  csbttc  37219