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

Theorem csbiegf 3905
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 1794 . 2 𝑥(𝑥 = 𝐴𝐵 = 𝐶)
3 csbiegf.1 . . 3 (𝐴𝑉𝑥𝐶)
4 csbiebt 3901 . . 3 ((𝐴𝑉𝑥𝐶) → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
53, 4mpdan 687 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝐵 = 𝐶) ↔ 𝐴 / 𝑥𝐵 = 𝐶))
62, 5mpbii 233 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537   = wceq 1539  wcel 2107  wnfc 2882  csb 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-v 3459  df-sbc 3764  df-csb 3873
This theorem is referenced by:  csbief  3906  sbcco3gw  4398  sbcco3g  4403  csbco3g  4404  fmptcof  7117  fmpoco  8089  sumsnf  15748  prodsn  15967  prodsnf  15969  bpolylem  16053  pcmpt  16899  chfacfpmmulfsupp  22788  elmptrab  23752  dvfsumrlim3  25979  itgsubstlem  25994  itgsubst  25995  ifeqeqx  32457  disjunsn  32509  sbcaltop  35928  unirep  37667  cdleme31so  40327  cdleme31sn  40328  cdleme31sn1  40329  cdleme31se  40330  cdleme31se2  40331  cdleme31sc  40332  cdleme31sde  40333  cdleme31sn2  40337  cdlemeg47rv2  40458  cdlemk41  40868  monotuz  42897  oddcomabszz  42900
  Copyright terms: Public domain W3C validator