Theorem csbconstg

Description: Substitution doesn't affect a constant B (in which x does not occur). csbconstgf with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012) Avoid ax-12 . (Revised by Gino Giotto, 15-Oct-2024)

	Ref	Expression
Assertion	csbconstg	|- ( A e. V -> [_ A / x ]_ B = B )

Proof

Step	Hyp	Ref	Expression
1		csbeq1	|- ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
2	1	eqeq1d	|- ( y = A -> ( [_ y / x ]_ B = B <-> [_ A / x ]_ B = B ) )
3		df-csb	|- [_ y / x ]_ B = { z | [. y / x ]. z e. B }
4		sbcg	|- ( y e. _V -> ( [. y / x ]. z e. B <-> z e. B ) )
5	4	elv	|- ( [. y / x ]. z e. B <-> z e. B )
6	5	abbii	|- { z | [. y / x ]. z e. B } = { z | z e. B }
7		abid2	|- { z | z e. B } = B
8	3 6 7	3eqtri	|- [_ y / x ]_ B = B
9	2 8	vtoclg	|- ( A e. V -> [_ A / x ]_ B = B )