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

Theorem csbprc 4355
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 3779 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1545 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 379 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2882 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3881 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1542 . . . 4 ¬ ⊥
76abf 4353 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2827 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2878 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wfal 1540  wcel 2105  {cab 2796  Vcvv 3492  [wsbc 3769  csb 3880  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-nul 4289
This theorem is referenced by:  csb0  4356  sbcel12  4357  sbcne12  4361  sbcel2  4364  csbidm  4379  csbun  4387  csbin  4388  csbif  4518  csbuni  4858  sbcbr123  5111  sbcbr  5112  csbexg  5205  csbopab  5433  csbxp  5643  csbres  5849  csbima12  5940  csbrn  6053  csbiota  6341  csbfv12  6706  csbfv  6708  csbriota  7118  csbov123  7187  csbov  7188  csbdif  34488
  Copyright terms: Public domain W3C validator