Theorem csbconstg 3869

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3868 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2215. (Revised by GG, 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 3853	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2764	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3851	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3814	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3458	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2829	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2899	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2789	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3520	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2740  Vcvv 3453  [wsbc 3742  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-sbc 3743  df-csb 3851

This theorem is used by:  csbconstgi  3871  csb0  4371  sbcel1g  4377  sbceq1g  4378  sbcel2  4379  sbceq2g  4380  csbidm  4394  2nreu  4405  csbopg  4854  sbcbr  5164  sbcbr12g  5165  sbcbr1g  5166  sbcbr2g  5167  csbmpt12  5540  csbmpt2  5541  sbcrel  5765  csbcnvgALTOLD  5872  csbres  5979  csbrn  6203  sbcfung  6561  csbfv12  6927  csbfv2g  6928  elfvmptrab  7020  csbov  7461  csbov12g  7462  csbov1g  7463  csbov2g  7464  csbfrecsg  8286  csbwrecsg  8320  csbwrdg  14611  gsummptif1n0  20097  coe1fzgsumdlem  22532  evl1gsumdlem  22585  opsbc2ie  32952  disjpreima  33059  esum2dlem  34604  csbrecsg  38084  csbrdgg  38085  csbmpo123  38087  f1omptsnlem  38092  relowlpssretop  38120  rdgeqoa  38126  csbfinxpg  38144  cdlemkid3N  41808  cdlemkid4  41809  cdlemk42  41816  minregex  44376  brtrclfv2  44569  cotrclrcl  44584  frege77  44782  onfrALTlem5  45367  onfrALTlem4  45368  onfrALTlem5VD  45709  onfrALTlem4VD  45710  csbsngVD  45717  csbxpgVD  45718  csbresgVD  45719  csbrngVD  45720  csbfv12gALTVD  45723  disjinfi  46026  eubrdm  47926  iccelpart  48335