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

Theorem csbiegf 3518
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 1711 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3514 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 698 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 221 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472   = wceq 1474  wcel 1975  wnfc 2733  csb 3494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
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 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-sbc 3398  df-csb 3495
This theorem is referenced by:  csbief  3519  sbcco3g  3946  csbco3g  3947  fmptcof  6285  fmpt2co  7120  sumsn  14261  prodsn  14473  prodsnf  14475  bpolylem  14560  pcmpt  15376  chfacfpmmulfsupp  20425  elmptrab  21378  dvfsumrlim3  23513  itgsubstlem  23528  itgsubst  23529  nbgraopALT  25715  ifeqeqx  28547  disjunsn  28591  sbcaltop  31060  unirep  32476  cdleme31so  34484  cdleme31sn  34485  cdleme31sn1  34486  cdleme31se  34487  cdleme31se2  34488  cdleme31sc  34489  cdleme31sde  34490  cdleme31sn2  34494  cdlemeg47rv2  34615  cdlemk41  35025  monotuz  36323  oddcomabszz  36326  sumsnf  38436
  Copyright terms: Public domain W3C validator