Theorem csbprc 4375

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 3766	. . . 4 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 → 𝐴 ∈ V)
2		falim 1557	. . . 4 ⊢ (⊥ → 𝐴 ∈ V)
3	1, 2	pm5.21ni 377	. . 3 ⊢ (¬ 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ ⊥))
4	3	abbidv 2796	. 2 ⊢ (¬ 𝐴 ∈ V → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ ⊥})
5		df-csb 3866	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		fal 1554	. . . 4 ⊢ ¬ ⊥
7	6	abf 4372	. . 3 ⊢ {𝑦 ∣ ⊥} = ∅
8	7	eqcomi 2739	. 2 ⊢ ∅ = {𝑦 ∣ ⊥}
9	4, 5, 8	3eqtr4g 2790	1 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ⊥wfal 1552   ∈ wcel 2109  {cab 2708  Vcvv 3450  [wsbc 3756  ⦋csb 3865  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-nul 4300

This theorem is referenced by:  csb0  4376  sbcel12  4377  sbcne12  4381  sbcel2  4384  csbidm  4399  csbun  4407  csbin  4408  csbdif  4490  csbif  4549  csbuni  4903  sbcbr123  5164  sbcbr  5165  csbexg  5268  csbopab  5518  csbxp  5741  csbres  5956  csbima12  6053  csbrn  6179  csbiota  6507  csbfv12  6909  csbfv  6911  csbriota  7362  csbov123  7434  csbov  7435