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

Theorem csbprc 3816
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 3431 . 2  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
2 sbcex 3336 . . . . . . 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 1388 . . . . 5  |-  ( F. 
->  [. A  /  x ]. y  e.  B
)
64, 5impbid1 203 . . . 4  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  <-> F.  ) )
76abbidv 2598 . . 3  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  | F.  }
)
8 fal 1381 . . . 4  |-  -. F.
98abf 3814 . . 3  |-  { y  | F.  }  =  (/)
107, 9syl6eq 2519 . 2  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  (/) )
111, 10syl5eq 2515 1  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ B  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1374   F. wfal 1379    e. wcel 1762   {cab 2447   _Vcvv 3108   [.wsbc 3326   [_csb 3430   (/)c0 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3781
This theorem is referenced by:  csb0  3817  sbcel12  3818  sbcne12  3822  sbcel2  3826  csbidm  3841  csbun  3852  csbin  3855  csbif  3984  csbuni  4268  sbcbr123  4493  sbcbr  4495  csbexg  4574  csbopab  4774  csbxp  5074  csbres  5269  csbima12  5347  csbrn  5461  csbiota  5573  csbfv12  5894  csbfv  5897  csbriota  6250  csbov123  6308  csbov  6309
  Copyright terms: Public domain W3C validator