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

Theorem csbied2 3917
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 2875 . . 3 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐵)
5 csbied2.3 . . 3 ((𝜑𝑥 = 𝐵) → 𝐶 = 𝐷)
64, 5syldan 591 . 2 ((𝜑𝑥 = 𝐴) → 𝐶 = 𝐷)
71, 6csbied 3916 1 (𝜑𝐴 / 𝑥𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  csb 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-sbc 3770  df-csb 3881
This theorem is referenced by:  prdsval  16716  cidfval  16935  monfval  16990  idfuval  17134  isnat  17205  fucco  17220  catcval  17344  xpcval  17415  1stfval  17429  2ndfval  17432  prfval  17437  evlf2  17456  curfval  17461  hofval  17490  ipoval  17752  poimirlem2  34775  rngcvalALTV  44160  ringcvalALTV  44206
  Copyright terms: Public domain W3C validator