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

Theorem sbcex 3597
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 3588 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 3364 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 207 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  {cab 2757  Vcvv 3351  [wsbc 3587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588
This theorem is referenced by:  sbcco  3610  sbc5  3612  sbcan  3630  sbcor  3631  sbcn1  3633  sbcim1  3634  sbcbi1  3635  sbcal  3637  sbcex2  3638  sbcel1v  3646  sbcel21v  3648  sbcimdv  3649  sbcrext  3661  sbcreu  3664  spesbc  3670  csbprc  4124  csbprcOLD  4125  sbcel12  4127  sbcne12  4130  sbcel2  4133  sbccsb2  4149  sbcbr123  4840  opelopabsb  5118  csbopab  5141  csbxp  5340  csbiota  6024  csbriota  6766  fi1uzind  13481  bj-csbprc  33233  sbccomieg  37883
  Copyright terms: Public domain W3C validator