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

Theorem csbiegf 3706
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 1870 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3702 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 667 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 223 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1629   = wceq 1631  wcel 2145  wnfc 2900  csb 3682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-sbc 3588  df-csb 3683
This theorem is referenced by:  csbief  3707  sbcco3g  4143  csbco3g  4144  fmptcof  6540  fmpt2co  7411  sumsnf  14681  sumsn  14683  prodsn  14899  prodsnf  14901  bpolylem  14985  pcmpt  15803  chfacfpmmulfsupp  20888  elmptrab  21851  dvfsumrlim3  24016  itgsubstlem  24031  itgsubst  24032  ifeqeqx  29699  disjunsn  29745  sbcaltop  32425  unirep  33839  cdleme31so  36188  cdleme31sn  36189  cdleme31sn1  36190  cdleme31se  36191  cdleme31se2  36192  cdleme31sc  36193  cdleme31sde  36194  cdleme31sn2  36198  cdlemeg47rv2  36319  cdlemk41  36729  monotuz  38032  oddcomabszz  38035
  Copyright terms: Public domain W3C validator