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

Theorem csbprc 3774
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 3350 . 2  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
2 sbcex 3265 . . . . . . 7  |-  ( [. A  /  x ]. y  e.  B  ->  A  e. 
_V )
32con3i 142 . . . . . 6  |-  ( -.  A  e.  _V  ->  -. 
[. A  /  x ]. y  e.  B
)
43pm2.21d 109 . . . . 5  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  -> F.  ) )
5 falim 1466 . . . . 5  |-  ( F. 
->  [. A  /  x ]. y  e.  B
)
64, 5impbid1 208 . . . 4  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  <-> F.  ) )
76abbidv 2589 . . 3  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  | F.  }
)
8 fal 1459 . . . 4  |-  -. F.
98abf 3772 . . 3  |-  { y  | F.  }  =  (/)
107, 9syl6eq 2521 . 2  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  (/) )
111, 10syl5eq 2517 1  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ B  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452   F. wfal 1457    e. wcel 1904   {cab 2457   _Vcvv 3031   [.wsbc 3255   [_csb 3349   (/)c0 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-in 3397  df-ss 3404  df-nul 3723
This theorem is referenced by:  csb0  3775  sbcel12  3776  sbcne12  3779  sbcel2  3782  csbidm  3795  csbun  3802  csbin  3803  csbif  3922  csbuni  4218  sbcbr123  4447  sbcbr  4448  csbexg  4530  csbopab  4733  csbxp  4921  csbres  5114  csbima12  5191  csbrn  5304  csbiota  5582  csbfv12  5914  csbfv  5916  csbriota  6282  csbov123  6342  csbov  6343  csbdif  31796
  Copyright terms: Public domain W3C validator