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

Theorem csbiegf 3775
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbiegf.1 (𝐴𝑉𝑥𝐶)
csbiegf.2 (𝑥 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
csbiegf (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem csbiegf
StepHypRef Expression
1 csbiegf.2 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
21ax-gen 1839 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3771 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 677 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 225 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1599   = wceq 1601  wcel 2107  wnfc 2919  csb 3751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-sbc 3653  df-csb 3752
This theorem is referenced by:  csbief  3776  sbcco3g  4224  csbco3g  4225  fmptcof  6662  fmpt2co  7541  sumsnf  14880  prodsn  15095  prodsnf  15097  bpolylem  15181  pcmpt  16000  chfacfpmmulfsupp  21075  elmptrab  22039  dvfsumrlim3  24233  itgsubstlem  24248  itgsubst  24249  ifeqeqx  29924  disjunsn  29970  sbcaltop  32677  unirep  34132  cdleme31so  36533  cdleme31sn  36534  cdleme31sn1  36535  cdleme31se  36536  cdleme31se2  36537  cdleme31sc  36538  cdleme31sde  36539  cdleme31sn2  36543  cdlemeg47rv2  36664  cdlemk41  37074  monotuz  38465  oddcomabszz  38468
  Copyright terms: Public domain W3C validator