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

Theorem sbcied 3689
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)
Hypotheses
Ref Expression
sbcied.1 (𝜑𝐴𝑉)
sbcied.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
sbcied (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem sbcied
StepHypRef Expression
1 sbcied.1 . 2 (𝜑𝐴𝑉)
2 sbcied.2 . 2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
3 nfv 1957 . 2 𝑥𝜑
4 nfvd 1958 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3688 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  [wsbc 3652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400  df-sbc 3653
This theorem is referenced by:  sbcied2  3690  sbc2iedv  3724  sbc3ie  3725  sbcralt  3728  euotd  5210  fmptsnd  6702  riota5f  6908  fpwwe2lem12  9798  fpwwe2lem13  9799  brfi1uzind  13594  opfi1uzind  13597  sbcie3s  16313  issubc  16880  gsumvalx  17656  dmdprd  18784  dprdval  18789  issrg  18894  issrng  19242  islmhm  19422  isassa  19712  isphl  20371  istmd  22286  istgp  22289  isnlm  22887  isclm  23271  iscph  23377  iscms  23551  limcfval  24073  ewlksfval  26949  sbcies  29894  abfmpeld  30019  abfmpel  30020  isomnd  30263  isorng  30361
  Copyright terms: Public domain W3C validator