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

Theorem sbcex 3478
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 3469 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 elex 3243 . 2 (𝐴 ∈ {𝑥𝜑} → 𝐴 ∈ V)
31, 2sylbi 207 1 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  {cab 2637  Vcvv 3231  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469
This theorem is referenced by:  sbcco  3491  sbc5  3493  sbcan  3511  sbcor  3512  sbcn1  3514  sbcim1  3515  sbcbi1  3516  sbcal  3518  sbcex2  3519  sbcel1v  3528  sbcel21v  3530  sbcimdv  3531  sbcimdvOLD  3532  sbcrext  3544  sbcrextOLD  3545  sbcreu  3548  spesbc  3554  csbprc  4013  csbprcOLD  4014  sbcel12  4016  sbcne12  4019  sbcel2  4022  sbccsb2  4038  sbcbr123  4739  opelopabsb  5014  csbopab  5037  csbxp  5234  csbiota  5919  csbriota  6663  fi1uzind  13317  bj-csbprc  33029  sbccomieg  37674
  Copyright terms: Public domain W3C validator