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

Theorem csbprc 3821
 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

Proof of Theorem csbprc
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-csb 3435 . 2
2 sbcex 3337 . . . . . . 7
32con3i 135 . . . . . 6
43pm2.21d 106 . . . . 5
5 falim 1409 . . . . 5
64, 5impbid1 203 . . . 4
76abbidv 2593 . . 3
8 fal 1402 . . . 4
98abf 3819 . . 3
107, 9syl6eq 2514 . 2
111, 10syl5eq 2510 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  =wceq 1395   wfal 1400  e.wcel 1818  {cab 2442   cvv 3109  [.wsbc 3327  [_csb 3434   c0 3784 This theorem is referenced by:  csb0  3822  sbcel12  3823  sbcne12  3827  sbcel2  3831  csbidm  3846  csbun  3857  csbin  3860  csbif  3991  csbuni  4277  sbcbr123  4503  sbcbr  4505  csbexg  4584  csbopab  4784  csbxp  5086  csbres  5281  csbima12  5359  csbrn  5473  csbiota  5585  csbfv12  5906  csbfv  5909  csbriota  6269  csbov123  6330  csbov  6331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785
 Copyright terms: Public domain W3C validator