Theorem csbief 3893

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

Step	Hyp	Ref	Expression
1		csbief.1	. 2 ⊢ 𝐴 ∈ V
2		csbief.2	. . . 4 ⊢ Ⅎ𝑥𝐶
3	2	a1i 11	. . 3 ⊢ (𝐴 ∈ V → Ⅎ𝑥𝐶)
4		csbief.3	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
5	3, 4	csbiegf 3892	. 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)
6	1, 5	ax-mp 5	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Ⅎwnfc 2882  Vcvv 3446  ⦋csb 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-v 3448  df-sbc 3743  df-csb 3859

This theorem is referenced by:  csbieOLD  3895  cbvrabcsfw  3902  csbun  4403  csbin  4404  csbdif  4490  csbif  4548  csbopab  5517  csbopabgALT  5518  csbima12  6036  csbcog  6254  csbiota  6494  csbriota  7334  csbov123  7404  pcmpt  16775  mpfrcl  21532  iundisj2  24950  iundisj2f  31575  iundisj2fi  31768  csbafv12g  45489  csbaovg  45532  csbafv212g  45571