Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbprc Structured version   Visualization version   GIF version

Theorem csbprc 4316
 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.
StepHypRef Expression
1 sbcex 3732 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1555 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 382 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2862 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3831 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1552 . . . 4 ¬ ⊥
76abf 4313 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2807 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2858 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538  ⊥wfal 1550   ∈ wcel 2111  {cab 2776  Vcvv 3442  [wsbc 3722  ⦋csb 3830  ∅c0 4246 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-nul 4247 This theorem is referenced by:  csb0  4317  csb0OLD  4318  sbcel12  4319  sbcne12  4323  sbcel2  4326  csbidm  4341  csbun  4349  csbin  4350  csbif  4483  csbuni  4833  sbcbr123  5088  sbcbr  5089  csbexg  5182  csbopab  5411  csbxp  5618  csbres  5825  csbima12  5918  csbrn  6031  csbiota  6325  csbfv12  6698  csbfv  6700  csbriota  7118  csbov123  7187  csbov  7188  csbdif  34893
 Copyright terms: Public domain W3C validator