Theorem csbiegf 3870

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 1801	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶)
3		csbiegf.1	. . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶)
4		csbiebt 3866	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
5	3, 4	mpdan 683	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
6	2, 5	mpbii 232	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541   ∈ wcel 2109  Ⅎwnfc 2888  ⦋csb 3836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-v 3432  df-sbc 3720  df-csb 3837

This theorem is referenced by:  csbief  3871  sbcco3gw  4361  sbcco3g  4366  csbco3g  4367  fmptcof  6996  fmpoco  7919  sumsnf  15436  prodsn  15653  prodsnf  15655  bpolylem  15739  pcmpt  16574  chfacfpmmulfsupp  21993  elmptrab  22959  dvfsumrlim3  25178  itgsubstlem  25193  itgsubst  25194  ifeqeqx  30864  disjunsn  30912  sbcaltop  34262  unirep  35850  cdleme31so  38372  cdleme31sn  38373  cdleme31sn1  38374  cdleme31se  38375  cdleme31se2  38376  cdleme31sc  38377  cdleme31sde  38378  cdleme31sn2  38382  cdlemeg47rv2  38503  cdlemk41  38913  monotuz  40743  oddcomabszz  40746