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

Theorem sbcied 3800
 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 1916 . 2 𝑥𝜑
4 nfvd 1917 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3799 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115  [wsbc 3758 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-sbc 3759 This theorem is referenced by:  sbcied2  3801  sbc2iedv  3835  sbc3ie  3836  sbcralt  3839  euotd  5390  fmptsnd  6922  riota5f  7135  fpwwe2lem12  10061  fpwwe2lem13  10062  brfi1uzind  13861  opfi1uzind  13864  sbcie3s  16541  issubc  17105  gsumvalx  17886  dmdprd  19120  dprdval  19125  issrg  19257  issrng  19621  islmhm  19799  isassa  20088  isphl  20772  istmd  22682  istgp  22685  isnlm  23284  isclm  23672  iscph  23778  iscms  23952  limcfval  24478  ewlksfval  27394  sbcies  30260  abfmpeld  30410  abfmpel  30411  isomnd  30734  isorng  30905
 Copyright terms: Public domain W3C validator