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

Theorem sbcied 3624
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 1995 . 2 𝑥𝜑
4 nfvd 1996 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3623 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  [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-10 2174  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588
This theorem is referenced by:  sbcied2  3625  sbc2iedv  3656  sbc3ie  3657  sbcralt  3660  euotd  5106  fmptsnd  6579  riota5f  6779  fpwwe2lem12  9665  fpwwe2lem13  9666  brfi1uzind  13482  opfi1uzind  13485  sbcie3s  16124  issubc  16702  gsumvalx  17478  dmdprd  18605  dprdval  18610  issrg  18715  issrng  19060  islmhm  19240  isassa  19530  isphl  20190  istmd  22098  istgp  22101  isnlm  22699  isclm  23083  iscph  23189  iscms  23361  limcfval  23856  ewlksfval  26732  sbcies  29662  abfmpeld  29794  abfmpel  29795  isomnd  30041  isorng  30139
  Copyright terms: Public domain W3C validator