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

Theorem sbcex 2972
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 2964 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 2749 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 121 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  {cab 2163  Vcvv 2738  [wsbc 2963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740  df-sbc 2964
This theorem is referenced by:  sbcco  2985  sbc5  2987  sbcan  3006  sbcor  3008  sbcn1  3011  sbcim1  3012  sbcbi1  3013  sbcal  3015  sbcex2  3017  sbcel1v  3026  sbcel21v  3028  sbcimdv  3029  sbcrext  3041  spesbc  3049  csbprc  3469  opelopabsb  4261
  Copyright terms: Public domain W3C validator