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

Theorem csbprc 4410
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 3788 . . . 4 ([𝐴 / 𝑥]𝑦𝐵𝐴 ∈ V)
2 falim 1550 . . . 4 (⊥ → 𝐴 ∈ V)
31, 2pm5.21ni 376 . . 3 𝐴 ∈ V → ([𝐴 / 𝑥]𝑦𝐵 ↔ ⊥))
43abbidv 2797 . 2 𝐴 ∈ V → {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦 ∣ ⊥})
5 df-csb 3895 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
6 fal 1547 . . . 4 ¬ ⊥
76abf 4406 . . 3 {𝑦 ∣ ⊥} = ∅
87eqcomi 2737 . 2 ∅ = {𝑦 ∣ ⊥}
94, 5, 83eqtr4g 2793 1 𝐴 ∈ V → 𝐴 / 𝑥𝐵 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wfal 1545  wcel 2098  {cab 2705  Vcvv 3473  [wsbc 3778  csb 3894  c0 4326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-nul 4327
This theorem is referenced by:  csb0  4411  sbcel12  4412  sbcne12  4416  sbcel2  4419  csbidm  4434  csbun  4442  csbin  4443  csbdif  4531  csbif  4589  csbuni  4943  sbcbr123  5206  sbcbr  5207  csbexg  5314  csbopab  5561  csbxp  5781  csbres  5992  csbima12  6087  csbrn  6212  csbiota  6546  csbfv12  6950  csbfv  6952  csbriota  7398  csbov123  7468  csbov  7469
  Copyright terms: Public domain W3C validator