Theorem csbconstg 3866

Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3865 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2182. (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 3850	. . 3 ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
2	1	eqeq1d 2735	. 2 ⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵))
3		df-csb 3848	. . 3 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵}
4		sbcg 3811	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
5	4	elv 3443	. . . 4 ⊢ ([𝑦 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
6	5	abbii 2800	. . 3 ⊢ {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐵} = {𝑧 ∣ 𝑧 ∈ 𝐵}
7		abid2 2870	. . 3 ⊢ {𝑧 ∣ 𝑧 ∈ 𝐵} = 𝐵
8	3, 6, 7	3eqtri 2760	. 2 ⊢ ⦋𝑦 / 𝑥⦌𝐵 = 𝐵
9	2, 8	vtoclg 3509	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2711  Vcvv 3438  [wsbc 3738  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-sbc 3739  df-csb 3848

This theorem is referenced by:  csbconstgi  3868  csb0  4361  sbcel1g  4367  sbceq1g  4368  sbcel2  4369  sbceq2g  4370  csbidm  4384  2nreu  4395  csbopg  4844  sbcbr  5150  sbcbr12g  5151  sbcbr1g  5152  sbcbr2g  5153  csbmpt12  5502  csbmpt2  5503  sbcrel  5727  csbcnvgALT  5831  csbres  5938  csbrn  6158  sbcfung  6513  csbfv12  6876  csbfv2g  6877  elfvmptrab  6967  csbov  7400  csbov12g  7401  csbov1g  7402  csbov2g  7403  csbfrecsg  8223  csbwrecsg  8257  csbwrdg  14461  gsummptif1n0  19888  coe1fzgsumdlem  22228  evl1gsumdlem  22281  opsbc2ie  32466  disjpreima  32575  esum2dlem  34116  csbrecsg  37383  csbrdgg  37384  csbmpo123  37386  f1omptsnlem  37391  relowlpssretop  37419  rdgeqoa  37425  csbfinxpg  37443  cdlemkid3N  41042  cdlemkid4  41043  cdlemk42  41050  minregex  43641  brtrclfv2  43834  cotrclrcl  43849  frege77  44047  onfrALTlem5  44649  onfrALTlem4  44650  onfrALTlem5VD  44991  onfrALTlem4VD  44992  csbsngVD  44999  csbxpgVD  45000  csbresgVD  45001  csbrngVD  45002  csbfv12gALTVD  45005  disjinfi  45303  eubrdm  47150  iccelpart  47547