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

Theorem sbcied 3622
 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 1994 . 2 𝑥𝜑
4 nfvd 1995 . 2 (𝜑 → Ⅎ𝑥𝜒)
51, 2, 3, 4sbciedf 3621 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1630   ∈ wcel 2144  [wsbc 3585 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-12 2202  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-v 3351  df-sbc 3586 This theorem is referenced by:  sbcied2  3623  sbc2iedv  3654  sbc3ie  3655  sbcralt  3658  euotd  5106  fmptsnd  6578  riota5f  6778  fpwwe2lem12  9664  fpwwe2lem13  9665  brfi1uzind  13481  opfi1uzind  13484  sbcie3s  16123  issubc  16701  gsumvalx  17477  dmdprd  18604  dprdval  18609  issrg  18714  issrng  19059  islmhm  19239  isassa  19529  isphl  20189  istmd  22097  istgp  22100  isnlm  22698  isclm  23082  iscph  23188  iscms  23360  limcfval  23855  ewlksfval  26731  sbcies  29656  abfmpeld  29788  abfmpel  29789  isomnd  30035  isorng  30133
 Copyright terms: Public domain W3C validator