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

Theorem sbcied 3454
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 1840 . 2 𝑥𝜑
4 nfvd 1841 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3453 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  [wsbc 3417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188  df-sbc 3418
This theorem is referenced by:  sbcied2  3455  sbc2iedv  3488  sbc3ie  3489  sbcralt  3492  euotd  4935  fmptsnd  6389  riota5f  6590  fpwwe2lem12  9407  fpwwe2lem13  9408  brfi1uzind  13219  opfi1uzind  13222  brfi1uzindOLD  13225  opfi1uzindOLD  13228  sbcie3s  15838  issubc  16416  gsumvalx  17191  dmdprd  18318  dprdval  18323  issrg  18428  issrng  18771  islmhm  18946  isassa  19234  isphl  19892  istmd  21788  istgp  21791  isnlm  22389  isclm  22772  iscph  22878  iscms  23050  limcfval  23542  ewlksfval  26367  sbcies  29171  abfmpeld  29296  abfmpel  29297  isomnd  29486  isorng  29584
  Copyright terms: Public domain W3C validator