Theorem csbconstg 3817

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3816 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2177. (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 3801	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2738	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3799	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3761	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3404	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2801	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2872	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2763	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3471	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  {cab 2714  Vcvv 3398  [wsbc 3683  ⦋csb 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-sbc 3684  df-csb 3799

This theorem is referenced by:  csbconstgi  3820  csb0  4308  sbcel1g  4314  sbceq1g  4315  sbcel2  4316  sbceq2g  4317  csbidm  4331  2nreu  4342  csbopg  4788  sbcbr  5094  sbcbr12g  5095  sbcbr1g  5096  sbcbr2g  5097  csbmpt12  5423  csbmpt2  5424  sbcrel  5637  csbcnvgALT  5738  csbres  5839  csbrn  6046  sbcfung  6382  csbfv12  6738  csbfv2g  6739  elfvmptrab  6824  csbov  7234  csbov12g  7235  csbov1g  7236  csbov2g  7237  csbwrdg  14064  gsummptif1n0  19305  coe1fzgsumdlem  21176  evl1gsumdlem  21226  opsbc2ie  30497  disjpreima  30596  esum2dlem  31726  csbwrecsg  35184  csbrecsg  35185  csbrdgg  35186  csbmpo123  35188  f1omptsnlem  35193  relowlpssretop  35221  rdgeqoa  35227  csbfinxpg  35245  cdlemkid3N  38633  cdlemkid4  38634  cdlemk42  38641  brtrclfv2  40953  cotrclrcl  40968  frege77  41166  onfrALTlem5  41776  onfrALTlem4  41777  onfrALTlem5VD  42119  onfrALTlem4VD  42120  csbsngVD  42127  csbxpgVD  42128  csbresgVD  42129  csbrngVD  42130  csbfv12gALTVD  42133  disjinfi  42345  eubrdm  44145  iccelpart  44501