Theorem csbprc 4272

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 3711	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1537	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 379	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2858	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3807	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1534	. . . 4 ⊢ ¬ ⊥
7	6	abf 4270	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2802	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2854	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1520  ⊥wfal 1532   ∈ wcel 2079  {cab 2773  Vcvv 3432  [wsbc 3701  ⦋csb 3806  ∅c0 4206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-fal 1533  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-nul 4207

This theorem is referenced by:  csb0  4273  sbcel12  4274  sbcne12  4278  sbcel2  4281  csbidm  4291  csbun  4299  csbin  4300  csbif  4430  csbuni  4767  sbcbr123  5010  sbcbr  5011  csbexg  5099  csbopab  5322  csbxp  5528  csbres  5729  csbima12  5815  csbrn  5927  csbiota  6210  csbfv12  6573  csbfv  6575  csbriota  6980  csbov123  7048  csbov  7049  csbdif  34083