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

Theorem csbprc 4367
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 3750 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1559 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 379 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2802 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3857 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1556 . . . 4 ¬ ⊥
76abf 4363 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2742 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2798 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wfal 1554  wcel 2107  {cab 2710  Vcvv 3444  [wsbc 3740  csb 3856  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-nul 4284
This theorem is referenced by:  csb0  4368  sbcel12  4369  sbcne12  4373  sbcel2  4376  csbidm  4391  csbun  4399  csbin  4400  csbdif  4486  csbif  4544  csbuni  4898  sbcbr123  5160  sbcbr  5161  csbexg  5268  csbopab  5513  csbxp  5732  csbres  5941  csbima12  6032  csbrn  6156  csbiota  6490  csbfv12  6891  csbfv  6893  csbriota  7330  csbov123  7400  csbov  7401
  Copyright terms: Public domain W3C validator