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

Theorem sbcex 3431
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 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)

Proof of Theorem sbcex
StepHypRef Expression
1 df-sbc 3422 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 3201 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 207 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  {cab 2607  Vcvv 3189  [wsbc 3421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3191  df-sbc 3422
This theorem is referenced by:  sbcco  3444  sbc5  3446  sbcan  3464  sbcor  3465  sbcn1  3467  sbcim1  3468  sbcbi1  3469  sbcal  3471  sbcex2  3472  sbcel1v  3481  sbcel21v  3483  sbcimdv  3484  sbcimdvOLD  3485  sbcrext  3497  sbcrextOLD  3498  sbcreu  3501  spesbc  3506  csbprc  3957  csbprcOLD  3958  sbcel12  3960  sbcne12  3963  sbcel2  3966  sbccsb2  3982  sbcbr123  4671  opelopabsb  4950  csbopab  4973  csbxp  5166  csbiota  5845  csbriota  6583  fi1uzind  13225  fi1uzindOLD  13231  bj-csbprc  32578  sbccomieg  36864
  Copyright terms: Public domain W3C validator