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

Theorem sbcied 3439
 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 1830 . 2 𝑥𝜑
4 nfvd 1831 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3438 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  [wsbc 3402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403 This theorem is referenced by:  sbcied2  3440  sbc2iedv  3473  sbc3ie  3474  sbcralt  3477  euotd  4900  fmptsnd  6340  riota5f  6535  fpwwe2lem12  9342  fpwwe2lem13  9343  brfi1uzind  13135  opfi1uzind  13138  brfi1uzindOLD  13141  opfi1uzindOLD  13144  sbcie3s  15745  issubc  16318  gsumvalx  17093  dmdprd  18220  dprdval  18225  issrg  18330  issrng  18673  islmhm  18848  isassa  19136  isphl  19792  istmd  21688  istgp  21691  isnlm  22289  isclm  22672  iscph  22778  iscms  22950  limcfval  23442  sbcies  28706  abfmpeld  28834  abfmpel  28835  isomnd  29032  isorng  29130  ewlksfval  40803
 Copyright terms: Public domain W3C validator