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

Theorem csbied2 3526
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 2665 . . 3 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐵)
5 csbied2.3 . . 3 ((𝜑𝑥 = 𝐵) → 𝐶 = 𝐷)
64, 5syldan 485 . 2 ((𝜑𝑥 = 𝐴) → 𝐶 = 𝐷)
71, 6csbied 3525 1 (𝜑𝐴 / 𝑥𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  csb 3498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-sbc 3402  df-csb 3499
This theorem is referenced by:  prdsval  15884  cidfval  16106  monfval  16161  idfuval  16305  isnat  16376  fucco  16391  catcval  16515  xpcval  16586  1stfval  16600  2ndfval  16603  prfval  16608  evlf2  16627  curfval  16632  hofval  16661  ipoval  16923  poimirlem2  32377  rngcvalALTV  41748  ringcvalALTV  41794
  Copyright terms: Public domain W3C validator