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

Theorem csbprc 3798
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 3396 . 2  |-  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
2 sbcex 3309 . . . . . . 7  |-  ( [. A  /  x ]. y  e.  B  ->  A  e. 
_V )
32con3i 140 . . . . . 6  |-  ( -.  A  e.  _V  ->  -. 
[. A  /  x ]. y  e.  B
)
43pm2.21d 109 . . . . 5  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  -> F.  ) )
5 falim 1451 . . . . 5  |-  ( F. 
->  [. A  /  x ]. y  e.  B
)
64, 5impbid1 206 . . . 4  |-  ( -.  A  e.  _V  ->  (
[. A  /  x ]. y  e.  B  <-> F.  ) )
76abbidv 2558 . . 3  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  {
y  | F.  }
)
8 fal 1444 . . . 4  |-  -. F.
98abf 3796 . . 3  |-  { y  | F.  }  =  (/)
107, 9syl6eq 2479 . 2  |-  ( -.  A  e.  _V  ->  { y  |  [. A  /  x ]. y  e.  B }  =  (/) )
111, 10syl5eq 2475 1  |-  ( -.  A  e.  _V  ->  [_ A  /  x ]_ B  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437   F. wfal 1442    e. wcel 1868   {cab 2407   _Vcvv 3081   [.wsbc 3299   [_csb 3395   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  csb0  3799  sbcel12  3800  sbcne12  3803  sbcel2  3806  csbidm  3819  csbun  3826  csbin  3827  csbif  3959  csbuni  4244  sbcbr123  4472  sbcbr  4473  csbexg  4554  csbopab  4748  csbxp  4931  csbres  5123  csbima12  5200  csbrn  5312  csbiota  5590  csbfv12  5912  csbfv  5914  csbriota  6275  csbov123  6335  csbov  6336  csbdif  31676
  Copyright terms: Public domain W3C validator