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

Theorem csbfv2g 6968
Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbfv2g (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐹𝐴 / 𝑥𝐵))
Distinct variable group:   𝑥,𝐹
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem csbfv2g
StepHypRef Expression
1 csbfv12 6967 . 2 𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)
2 csbconstg 3934 . . 3 (𝐴𝐶𝐴 / 𝑥𝐹 = 𝐹)
32fveq1d 6921 . 2 (𝐴𝐶 → (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = (𝐹𝐴 / 𝑥𝐵))
41, 3eqtrid 2786 1 (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐹𝐴 / 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2103  csb 3915  cfv 6572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-nul 5327  ax-pr 5450
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ral 3064  df-rex 3073  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-ss 3987  df-nul 4348  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-dm 5709  df-iota 6524  df-fv 6580
This theorem is referenced by:  csbfv  6969  ixpsnval  8954  swrdspsleq  14709  sumeq2ii  15737  fsumabs  15845  prodeq2ii  15955  fprodabs  16016  ixpsnbasval  21233  coe1fzgsumdlem  22321  evl1gsumdlem  22374  pm2mp  22845  cayhamlem4  22908  iuninc  32574  cdlemk39s  40844  evl1gprodd  42022  minregex  43436
  Copyright terms: Public domain W3C validator