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

Theorem csbiegf 3898
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 group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem csbiegf
StepHypRef Expression
1 csbiegf.2 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
21ax-gen 1795 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3894 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 687 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 233 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538   = wceq 1540  wcel 2109  wnfc 2877  csb 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-v 3452  df-sbc 3757  df-csb 3866
This theorem is referenced by:  csbief  3899  sbcco3gw  4391  sbcco3g  4396  csbco3g  4397  fmptcof  7105  fmpoco  8077  sumsnf  15716  prodsn  15935  prodsnf  15937  bpolylem  16021  pcmpt  16870  chfacfpmmulfsupp  22757  elmptrab  23721  dvfsumrlim3  25947  itgsubstlem  25962  itgsubst  25963  ifeqeqx  32478  disjunsn  32530  sbcaltop  35976  unirep  37715  cdleme31so  40380  cdleme31sn  40381  cdleme31sn1  40382  cdleme31se  40383  cdleme31se2  40384  cdleme31sc  40385  cdleme31sde  40386  cdleme31sn2  40390  cdlemeg47rv2  40511  cdlemk41  40921  monotuz  42937  oddcomabszz  42940
  Copyright terms: Public domain W3C validator