Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbcex GIF version

Theorem sbcex 2917
 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 2910 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 2697 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 120 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1480  {cab 2125  Vcvv 2686  [wsbc 2909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688  df-sbc 2910 This theorem is referenced by:  sbcco  2930  sbc5  2932  sbcan  2951  sbcor  2953  sbcn1  2956  sbcim1  2957  sbcbi1  2958  sbcal  2960  sbcex2  2962  sbcel1v  2971  sbcel21v  2973  sbcimdv  2974  sbcrext  2986  spesbc  2994  csbprc  3408  opelopabsb  4182
 Copyright terms: Public domain W3C validator