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

Theorem sbcied2 3743
 Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)
Hypotheses
Ref Expression
sbcied2.1 (𝜑𝐴𝑉)
sbcied2.2 (𝜑𝐴 = 𝐵)
sbcied2.3 ((𝜑𝑥 = 𝐵) → (𝜓𝜒))
Assertion
Ref Expression
sbcied2 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem sbcied2
StepHypRef Expression
1 sbcied2.1 . 2 (𝜑𝐴𝑉)
2 id 22 . . . 4 (𝑥 = 𝐴𝑥 = 𝐴)
3 sbcied2.2 . . . 4 (𝜑𝐴 = 𝐵)
42, 3sylan9eqr 2816 . . 3 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐵)
5 sbcied2.3 . . 3 ((𝜑𝑥 = 𝐵) → (𝜓𝜒))
64, 5syldan 594 . 2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
71, 6sbcied 3742 1 (𝜑 → ([𝐴 / 𝑥]𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  [wsbc 3699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-sbc 3700 This theorem is referenced by:  iscat  17016  sectffval  17094  issubc  17179  isfunc  17208  ismgm  17934  issgrp  17983  isnsg  18389  isring  19384  islbs  19931  isdomn  20150  isassa  20636  opsrval  20821  isuhgr  26967  isushgr  26968  isupgr  26991  isumgr  27002  isuspgr  27059  isusgr  27060  isrng  44927
 Copyright terms: Public domain W3C validator