Theorem csbconstg 3140

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). csbconstgf 3139 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 2373	. 2 ⊢ Ⅎ𝑥𝐵
2	1	csbconstgf 3139	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  ⦋csb 3126

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-sbc 3031  df-csb 3127

This theorem is referenced by:  sbcel1g  3145  sbceq1g  3146  sbcel2g  3147  sbceq2g  3148  csbidmg  3183  sbcbr12g  4145  sbcbr1g  4146  sbcbr2g  4147  sbcrel  4814  csbcnvg  4916  csbresg  5018  sbcfung  5352  csbfv12g  5682  csbfv2g  5683  elfvmptrab  5745  csbov12g  6063  csbov1g  6064  csbov2g  6065  csbwrdg  11152