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

Theorem sbcex 3798
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 3789 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 3501 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 217 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  {cab 2714  Vcvv 3480  [wsbc 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sbc 3789
This theorem is referenced by:  sbccow  3811  sbcco  3814  sbc5ALT  3817  sbcan  3838  sbcor  3839  sbcn1  3841  sbcim1  3842  sbcim1OLD  3843  sbcbi1  3847  sbcal  3849  sbcex2  3850  sbcel1v  3856  sbcel21v  3858  sbccomlem  3869  sbcrext  3873  sbcreu  3876  spesbc  3882  csbprc  4409  sbcel12  4411  sbcne12  4415  sbcel2  4418  sbccsb2  4437  sbcbr123  5197  opelopabsb  5535  csbopab  5560  csbxp  5785  csbiota  6554  csbriota  7403  fi1uzind  14546  bj-csbprc  36911  sbccomieg  42804
  Copyright terms: Public domain W3C validator