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

Theorem csbief 3920
 Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbief.1 𝐴 ∈ V
csbief.2 𝑥𝐶
csbief.3 (𝑥 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
csbief 𝐴 / 𝑥𝐵 = 𝐶
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem csbief
StepHypRef Expression
1 csbief.1 . 2 𝐴 ∈ V
2 csbief.2 . . . 4 𝑥𝐶
32a1i 11 . . 3 (𝐴 ∈ V → 𝑥𝐶)
4 csbief.3 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
53, 4csbiegf 3919 . 2 (𝐴 ∈ V → 𝐴 / 𝑥𝐵 = 𝐶)
61, 5ax-mp 5 1 𝐴 / 𝑥𝐵 = 𝐶
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  Ⅎwnfc 2964  Vcvv 3497  ⦋csb 3886 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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-sbc 3776  df-csb 3887 This theorem is referenced by:  csbie  3921  cbvrabcsfw  3927  csbun  4393  csbin  4394  csbif  4525  csbopab  5445  csbopabgALT  5446  csbima12  5950  csbiota  6351  csbriota  7132  csbov123  7201  pcmpt  16231  mpfrcl  20301  iundisj2  24153  iundisj2f  30343  iundisj2fi  30523  csbdif  34610  csbcog  40000  csbafv12g  43343  csbaovg  43386  csbafv212g  43425
 Copyright terms: Public domain W3C validator