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

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

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