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

Theorem sbcied 3819
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ax-10 2129, ax-12 2166. (Revised by GG, 12-Oct-2024.)
Hypotheses
Ref Expression
sbcied.1 (𝜑𝐴𝑉)
sbcied.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
sbcied (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem sbcied
StepHypRef Expression
1 df-sbc 3774 . 2 ([𝐴 / 𝑥]𝜓𝐴 ∈ {𝑥𝜓})
2 sbcied.1 . . 3 (𝜑𝐴𝑉)
3 sbcied.2 . . 3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
42, 3elabd3 3656 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜒))
51, 4bitrid 282 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  {cab 2702  [wsbc 3773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3774
This theorem is referenced by:  sbcied2  3821  sbc2ie  3856  sbc2iedv  3858  sbc3ie  3859  sbcralt  3862  csbied  3927  euotd  5515  fmptsnd  7178  riota5f  7404  fpwwe2lem11  10666  fpwwe2lem12  10667  brfi1uzind  14495  opfi1uzind  14498  sbcie3s  17134  issubc  17824  gsumvalx  18639  dmdprd  19967  dprdval  19972  issrg  20140  issrng  20742  islmhm  20924  isphl  21577  istmd  24022  istgp  24025  isnlm  24636  isclm  25035  iscph  25142  iscms  25317  limcfval  25845  ewlksfval  29487  sbcies  32364  abfmpeld  32521  abfmpel  32522  isomnd  32871  isorng  33113  rprmval  33328  f1o2d2  41857
  Copyright terms: Public domain W3C validator