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

Theorem csbprc 3952
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 3427 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1495 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 367 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2738 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3515 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1487 . . . 4 ¬ ⊥
76abf 3950 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2630 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2680 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wfal 1485  wcel 1987  {cab 2607  Vcvv 3186  [wsbc 3417  csb 3514  c0 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-nul 3892
This theorem is referenced by:  csb0  3954  sbcel12  3955  sbcne12  3958  sbcel2  3961  csbidm  3974  csbun  3981  csbin  3982  csbif  4110  csbuni  4432  sbcbr123  4666  sbcbr  4667  csbexg  4752  csbopab  4968  csbxp  5161  csbres  5359  csbima12  5442  csbrn  5555  csbiota  5840  csbfv12  6188  csbfv  6190  csbriota  6577  csbov123  6640  csbov  6641  csbdif  32803
  Copyright terms: Public domain W3C validator