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

Theorem sbcex 3781
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 3772 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 3513 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 218 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  {cab 2799  Vcvv 3495  [wsbc 3771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3497  df-sbc 3772
This theorem is referenced by:  sbccow  3794  sbcco  3797  sbc5  3799  sbcan  3820  sbcor  3821  sbcn1  3823  sbcim1  3824  sbcbi1  3829  sbcal  3832  sbcex2  3833  sbcel1v  3838  sbcel1vOLD  3839  sbcel21v  3841  sbcimdv  3842  sbcrext  3855  sbcreu  3858  spesbc  3864  csbprc  4357  sbcel12  4359  sbcne12  4363  sbcel2  4366  sbccsb2  4385  sbcbr123  5112  opelopabsb  5409  csbopab  5434  csbxp  5644  csbiota  6342  csbriota  7118  fi1uzind  13845  bj-csbprc  34124  sbccomieg  39270
  Copyright terms: Public domain W3C validator