Theorem csbprc 4373

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569  ⊥wfal 1581   ∈ wcel 2142  {cab 2740  Vcvv 3454  [wsbc 3743  ⦋csb 3852  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-nul 4286

This theorem is used by:  csb0  4374  sbcel12  4375  sbcne12  4379  sbcel2  4382  csbidm  4397  csbun  4405  csbin  4406  csbdif  4485  csbif  4544  csbuni  4902  sbcbr123  5164  sbcbr  5165  csbexg  5272  csbopab  5539  csbxp  5761  csbcnv  5871  csbres  5980  csbima12  6080  csbrn  6203  csbiota  6529  csbfv12  6926  csbfv  6928  csbriota  7384  csbov123  7456  csbov  7457  csbttc  37048