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

Theorem sbcex 3337
Description: By our definition of proper substitution, it can only be true if the substituted expression is a set. (Contributed by Mario Carneiro, 13-Oct-2016.)
Assertion
Ref Expression
sbcex

Proof of Theorem sbcex
StepHypRef Expression
1 df-sbc 3328 . 2
2 elex 3118 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  {cab 2442   cvv 3109  [.wsbc 3327
This theorem is referenced by:  sbcco  3350  sbc5  3352  sbcan  3370  sbcor  3372  sbcn1  3375  sbcim1  3376  sbcbi1  3377  sbcal  3379  sbcex2  3381  sbcel1v  3392  sbcel21v  3395  sbcimdv  3396  sbcrext  3410  sbcreu  3414  spesbc  3420  csbprc  3821  sbcel12  3823  sbcne12  3827  sbcel2  3831  sbccsb2  3851  sbcbr123  4503  opelopabsb  4762  csbopab  4784  csbxp  5086  csbiota  5585  csbriota  6269  sbccomieg  30726  bj-csbprc  34476
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-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328
  Copyright terms: Public domain W3C validator