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

Theorem csbprc 3672
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.)
Assertion
Ref Expression
csbprc  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ B  =  (/) )

Proof of Theorem csbprc
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-csb 3288 . 2  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
2 sbcex 3195 . . . . . . 7  |-  ( [. A  /  x ]. y  e.  B  ->  A  e. 
_V )
32con3i 135 . . . . . 6  |-  ( -.  A  e.  _V  ->  -. 
[. A  /  x ]. y  e.  B
)
43pm2.21d 106 . . . . 5  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  -> F.  ) )
5 falim 1383 . . . . 5  |-  ( F. 
->  [. A  /  x ]. y  e.  B
)
64, 5impbid1 203 . . . 4  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  <-> F.  ) )
76abbidv 2556 . . 3  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  | F.  }
)
8 fal 1376 . . . 4  |-  -. F.
98abf 3670 . . 3  |-  { y  | F.  }  =  (/)
107, 9syl6eq 2490 . 2  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  (/) )
111, 10syl5eq 2486 1  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ B  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369   F. wfal 1374    e. wcel 1756   {cab 2428   _Vcvv 2971   [.wsbc 3185   [_csb 3287   (/)c0 3636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-in 3334  df-ss 3341  df-nul 3637
This theorem is referenced by:  csb0  3673  sbcel12  3674  sbcne12  3678  sbcel2  3682  csbidm  3697  csbun  3708  csbin  3711  csbif  3838  csbuni  4118  sbcbr123  4342  sbcbr  4344  csbexg  4423  csbopab  4619  csbxp  4917  csbres  5112  csbima12  5185  csbrn  5298  csbiota  5409  csbfv12  5724  csbfv  5727  csbriota  6063  csbov123  6121  csbov  6122
  Copyright terms: Public domain W3C validator