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

Theorem csbprc 4172
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 3637 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1655 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 368 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2921 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3723 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1652 . . . 4 ¬ ⊥
76abf 4170 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2811 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2861 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1637  wfal 1650  wcel 2155  {cab 2788  Vcvv 3387  [wsbc 3627  csb 3722  c0 4110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-nul 4111
This theorem is referenced by:  csb0  4173  sbcel12  4174  sbcne12  4177  sbcel2  4180  csbidm  4193  csbun  4201  csbin  4202  csbif  4328  csbuni  4653  sbcbr123  4891  sbcbr  4892  csbexg  4981  csbopab  5197  csbxp  5396  csbres  5594  csbima12  5687  csbrn  5801  csbiota  6088  csbfv12  6445  csbfv  6447  csbriota  6841  csbov123  6909  csbov  6910  csbdif  33482
  Copyright terms: Public domain W3C validator