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

Theorem csbprc 4272
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 3711 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1537 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 379 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2858 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3807 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1534 . . . 4 ¬ ⊥
76abf 4270 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2802 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2854 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1520  wfal 1532  wcel 2079  {cab 2773  Vcvv 3432  [wsbc 3701  csb 3806  c0 4206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-fal 1533  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-nul 4207
This theorem is referenced by:  csb0  4273  sbcel12  4274  sbcne12  4278  sbcel2  4281  csbidm  4291  csbun  4299  csbin  4300  csbif  4430  csbuni  4767  sbcbr123  5010  sbcbr  5011  csbexg  5099  csbopab  5322  csbxp  5528  csbres  5729  csbima12  5815  csbrn  5927  csbiota  6210  csbfv12  6573  csbfv  6575  csbriota  6980  csbov123  7048  csbov  7049  csbdif  34083
  Copyright terms: Public domain W3C validator