Theorem sbceqbii

Description: Formula-building inference for class substitution. General version of sbcbii . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	sbceqbii.1	|- A = B
	sbceqbii.2	|- ( ph <-> ps )
Assertion	sbceqbii	|- ( [. A / x ]. ph <-> [. B / x ]. ps )

Proof

Step	Hyp	Ref	Expression
1		sbceqbii.1	|- A = B
2		sbceqbii.2	|- ( ph <-> ps )
3	2	abbii	|- { x | ph } = { x | ps }
4	1 3	eleq12i	|- ( A e. { x | ph } <-> B e. { x | ps } )
5		df-sbc	|- ( [. A / x ]. ph <-> A e. { x | ph } )
6		df-sbc	|- ( [. B / x ]. ps <-> B e. { x | ps } )
7	4 5 6	3bitr4i	|- ( [. A / x ]. ph <-> [. B / x ]. ps )