Theorem csbconstg 3141

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). csbconstgf 3140 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)

Assertion

Ref	Expression
csbconstg	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Distinct variable group:   𝑥,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem csbconstg

Step	Hyp	Ref	Expression
1		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐵
2	1	csbconstgf 3140	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  ⦋csb 3127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sbc 3032  df-csb 3128

This theorem is referenced by:  sbcel1g  3146  sbceq1g  3147  sbcel2g  3148  sbceq2g  3149  csbidmg  3184  sbcbr12g  4144  sbcbr1g  4145  sbcbr2g  4146  sbcrel  4812  csbcnvg  4914  csbresg  5016  sbcfung  5350  csbfv12g  5679  csbfv2g  5680  elfvmptrab  5742  csbov12g  6058  csbov1g  6059  csbov2g  6060  csbwrdg  11144