Theorem csbconstg 3871

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {cab 2739  Vcvv 3453  [wsbc 3743  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-sbc 3744  df-csb 3853

This theorem is referenced by:  csbconstgi  3873  csb0  4374  sbcel1g  4380  sbceq1g  4381  sbcel2  4382  sbceq2g  4383  csbidm  4397  2nreu  4408  csbopg  4855  sbcbr  5165  sbcbr12g  5166  sbcbr1g  5167  sbcbr2g  5168  csbmpt12  5542  csbmpt2  5543  sbcrel  5767  csbcnvgALTOLD  5874  csbres  5981  csbrn  6204  sbcfung  6560  csbfv12  6926  csbfv2g  6927  elfvmptrab  7019  csbov  7455  csbov12g  7456  csbov1g  7457  csbov2g  7458  csbfrecsg  8280  csbwrecsg  8314  csbwrdg  14581  gsummptif1n0  20035  coe1fzgsumdlem  22442  evl1gsumdlem  22495  opsbc2ie  32788  disjpreima  32895  esum2dlem  34448  csbrecsg  37940  csbrdgg  37941  csbmpo123  37943  f1omptsnlem  37948  relowlpssretop  37976  rdgeqoa  37982  csbfinxpg  38000  cdlemkid3N  41675  cdlemkid4  41676  cdlemk42  41683  minregex  44230  brtrclfv2  44423  cotrclrcl  44438  frege77  44636  onfrALTlem5  45221  onfrALTlem4  45222  onfrALTlem5VD  45563  onfrALTlem4VD  45564  csbsngVD  45571  csbxpgVD  45572  csbresgVD  45573  csbrngVD  45574  csbfv12gALTVD  45577  disjinfi  45880  eubrdm  47740  iccelpart  48149