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

Theorem csbied2 3936
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
csbied2.1 (𝜑𝐴𝑉)
csbied2.2 (𝜑𝐴 = 𝐵)
csbied2.3 ((𝜑𝑥 = 𝐵) → 𝐶 = 𝐷)
Assertion
Ref Expression
csbied2 (𝜑𝐴 / 𝑥𝐶 = 𝐷)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem csbied2
StepHypRef Expression
1 csbied2.1 . 2 (𝜑𝐴𝑉)
2 id 22 . . . 4 (𝑥 = 𝐴𝑥 = 𝐴)
3 csbied2.2 . . . 4 (𝜑𝐴 = 𝐵)
42, 3sylan9eqr 2799 . . 3 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐵)
5 csbied2.3 . . 3 ((𝜑𝑥 = 𝐵) → 𝐶 = 𝐷)
64, 5syldan 591 . 2 ((𝜑𝑥 = 𝐴) → 𝐶 = 𝐷)
71, 6csbied 3935 1 (𝜑𝐴 / 𝑥𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  csb 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900
This theorem is referenced by:  prdsval  17500  cidfval  17719  monfval  17776  idfuval  17921  isnat  17995  fucco  18010  catcval  18145  xpcval  18222  1stfval  18236  2ndfval  18239  prfval  18244  evlf2  18263  curfval  18268  hofval  18297  ipoval  18575  mntoval  32972  mgcoval  32976  erlval  33262  rlocval  33263  poimirlem2  37629  rngcvalALTV  48181  ringcvalALTV  48205  upfval  48933  swapfval  48968  fucofvalg  49013  fuco21  49031
  Copyright terms: Public domain W3C validator