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

Theorem sbcied 3832
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ax-10 2141, ax-12 2177. (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 3789 . 2 ([𝐴 / 𝑥]𝜓𝐴 ∈ {𝑥𝜓})
2 sbcied.1 . . 3 (𝜑𝐴𝑉)
3 sbcied.2 . . 3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
42, 3elabd3 3671 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜒))
51, 4bitrid 283 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  [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-sbc 3789
This theorem is referenced by:  sbcied2  3833  sbc2ie  3866  sbc2iedv  3867  sbc3ie  3868  sbcralt  3872  csbied  3935  euotd  5518  fmptsnd  7189  riota5f  7416  fpwwe2lem11  10681  fpwwe2lem12  10682  brfi1uzind  14547  opfi1uzind  14550  sbcie3s  17199  issubc  17880  gsumvalx  18689  dmdprd  20018  dprdval  20023  issrg  20185  issrng  20845  islmhm  21026  isphl  21646  istmd  24082  istgp  24085  isnlm  24696  isclm  25097  iscph  25204  iscms  25379  limcfval  25907  ewlksfval  29619  sbcies  32507  abfmpeld  32664  abfmpel  32665  isomnd  33078  isorng  33329  rprmval  33544  f1o2d2  42274
  Copyright terms: Public domain W3C validator