Theorem csbiegf 3706

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

Step	Hyp	Ref	Expression
1		csbiegf.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
2	1	ax-gen 1870	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶)
3		csbiegf.1	. . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶)
4		csbiebt 3702	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
5	3, 4	mpdan 667	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
6	2, 5	mpbii 223	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1629   = wceq 1631   ∈ wcel 2145  Ⅎwnfc 2900  ⦋csb 3682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-sbc 3588  df-csb 3683

This theorem is referenced by:  csbief  3707  sbcco3g  4143  csbco3g  4144  fmptcof  6540  fmpt2co  7411  sumsnf  14681  sumsn  14683  prodsn  14899  prodsnf  14901  bpolylem  14985  pcmpt  15803  chfacfpmmulfsupp  20888  elmptrab  21851  dvfsumrlim3  24016  itgsubstlem  24031  itgsubst  24032  ifeqeqx  29699  disjunsn  29745  sbcaltop  32425  unirep  33839  cdleme31so  36188  cdleme31sn  36189  cdleme31sn1  36190  cdleme31se  36191  cdleme31se2  36192  cdleme31sc  36193  cdleme31sde  36194  cdleme31sn2  36198  cdlemeg47rv2  36319  cdlemk41  36729  monotuz  38032  oddcomabszz  38035