Theorem csbprc 4406

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 3787	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1558	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 378	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2801	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3894	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1555	. . . 4 ⊢ ¬ ⊥
7	6	abf 4402	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2741	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2797	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ⊥wfal 1553   ∈ wcel 2106  {cab 2709  Vcvv 3474  [wsbc 3777  ⦋csb 3893  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-nul 4323

This theorem is referenced by:  csb0  4407  sbcel12  4408  sbcne12  4412  sbcel2  4415  csbidm  4430  csbun  4438  csbin  4439  csbdif  4527  csbif  4585  csbuni  4940  sbcbr123  5202  sbcbr  5203  csbexg  5310  csbopab  5555  csbxp  5775  csbres  5984  csbima12  6078  csbrn  6202  csbiota  6536  csbfv12  6939  csbfv  6941  csbriota  7380  csbov123  7450  csbov  7451