Theorem csbprc 4344

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 3740	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1564	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 378	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2806	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3839	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		dfnul4 4270	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
7	4, 5, 6	3eqtr4g 2800	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547  ⊥wfal 1559   ∈ wcel 2119  {cab 2718  Vcvv 3432  [wsbc 3730  ⦋csb 3838  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-nul 4269

This theorem is referenced by:  csb0  4345  sbcel12  4346  sbcne12  4350  sbcel2  4353  csbidm  4368  csbun  4376  csbin  4377  csbdif  4460  csbif  4519  csbuni  4875  sbcbr123  5133  sbcbr  5134  csbexg  5239  csbopab  5504  csbxp  5726  csbres  5941  csbima12  6038  csbrn  6161  csbiota  6485  csbfv12  6879  csbfv  6881  csbriota  7335  csbov123  7407  csbov  7408  csbttc  36738