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

Theorem sbcex 2795
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 2788 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 2583 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 118 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  {cab 2042  Vcvv 2574  [wsbc 2787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-v 2576  df-sbc 2788
This theorem is referenced by:  sbcco  2808  sbc5  2810  sbcan  2828  sbcor  2830  sbcn1  2833  sbcim1  2834  sbcbi1  2835  sbcal  2837  sbcex2  2839  sbcel1v  2848  sbcel21v  2850  sbcimdv  2851  sbcrext  2863  spesbc  2871  csbprc  3290  opelopabsb  4025
  Copyright terms: Public domain W3C validator