Theorem csbconstg 3908

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3907 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2164. (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 3892	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2729	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3890	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3852	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3475	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2797	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2866	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2759	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3538	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {cab 2704  Vcvv 3469  [wsbc 3774  ⦋csb 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-sbc 3775  df-csb 3890

This theorem is referenced by:  csbconstgi  3911  csb0  4403  sbcel1g  4409  sbceq1g  4410  sbcel2  4411  sbceq2g  4412  csbidm  4426  2nreu  4437  csbopg  4887  sbcbr  5197  sbcbr12g  5198  sbcbr1g  5199  sbcbr2g  5200  csbmpt12  5553  csbmpt2  5554  sbcrel  5776  csbcnvgALT  5881  csbres  5982  csbrn  6201  sbcfung  6571  csbfv12  6939  csbfv2g  6940  elfvmptrab  7028  csbov  7457  csbov12g  7458  csbov1g  7459  csbov2g  7460  csbfrecsg  8283  csbwrecsg  8320  csbwrdg  14518  gsummptif1n0  19912  coe1fzgsumdlem  22209  evl1gsumdlem  22262  opsbc2ie  32260  disjpreima  32359  esum2dlem  33647  csbrecsg  36743  csbrdgg  36744  csbmpo123  36746  f1omptsnlem  36751  relowlpssretop  36779  rdgeqoa  36785  csbfinxpg  36803  cdlemkid3N  40343  cdlemkid4  40344  cdlemk42  40351  minregex  42887  brtrclfv2  43080  cotrclrcl  43095  frege77  43293  onfrALTlem5  43904  onfrALTlem4  43905  onfrALTlem5VD  44247  onfrALTlem4VD  44248  csbsngVD  44255  csbxpgVD  44256  csbresgVD  44257  csbrngVD  44258  csbfv12gALTVD  44261  disjinfi  44488  eubrdm  46341  iccelpart  46696