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

Theorem csbiegf 3543
 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 1719 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3539 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 701 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 223 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1478   = wceq 1480   ∈ wcel 1987  Ⅎwnfc 2748  ⦋csb 3519 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-sbc 3423  df-csb 3520 This theorem is referenced by:  csbief  3544  sbcco3g  3977  csbco3g  3978  fmptcof  6363  fmpt2co  7220  sumsnf  14422  sumsn  14424  prodsn  14636  prodsnf  14638  bpolylem  14723  pcmpt  15539  chfacfpmmulfsupp  20608  elmptrab  21570  dvfsumrlim3  23734  itgsubstlem  23749  itgsubst  23750  ifeqeqx  29249  disjunsn  29293  sbcaltop  31783  unirep  33178  cdleme31so  35186  cdleme31sn  35187  cdleme31sn1  35188  cdleme31se  35189  cdleme31se2  35190  cdleme31sc  35191  cdleme31sde  35192  cdleme31sn2  35196  cdlemeg47rv2  35317  cdlemk41  35727  monotuz  37025  oddcomabszz  37028
 Copyright terms: Public domain W3C validator