Theorem csbconstg 3856

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3855 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2169. (Revised by Gino Giotto, 15-Oct-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐵

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

Proof of Theorem csbconstg

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq1 3840	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2738	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3838	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3800	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3443	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2806	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2880	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2768	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3510	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {cab 2713  Vcvv 3437  [wsbc 3721  ⦋csb 3837

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-sbc 3722  df-csb 3838

This theorem is referenced by:  csbconstgi  3859  csb0  4347  sbcel1g  4353  sbceq1g  4354  sbcel2  4355  sbceq2g  4356  csbidm  4370  2nreu  4381  csbopg  4827  sbcbr  5136  sbcbr12g  5137  sbcbr1g  5138  sbcbr2g  5139  csbmpt12  5483  csbmpt2  5484  sbcrel  5702  csbcnvgALT  5806  csbres  5906  csbrn  6121  sbcfung  6487  csbfv12  6849  csbfv2g  6850  elfvmptrab  6935  csbov  7350  csbov12g  7351  csbov1g  7352  csbov2g  7353  csbfrecsg  8131  csbwrecsg  8168  csbwrdg  14292  gsummptif1n0  19612  coe1fzgsumdlem  21517  evl1gsumdlem  21567  opsbc2ie  30869  disjpreima  30968  esum2dlem  32105  csbrecsg  35543  csbrdgg  35544  csbmpo123  35546  f1omptsnlem  35551  relowlpssretop  35579  rdgeqoa  35585  csbfinxpg  35603  cdlemkid3N  38989  cdlemkid4  38990  cdlemk42  38997  minregex  41179  brtrclfv2  41373  cotrclrcl  41388  frege77  41586  onfrALTlem5  42200  onfrALTlem4  42201  onfrALTlem5VD  42543  onfrALTlem4VD  42544  csbsngVD  42551  csbxpgVD  42552  csbresgVD  42553  csbrngVD  42554  csbfv12gALTVD  42557  disjinfi  42775  eubrdm  44588  iccelpart  44943