Theorem sbceqbii

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

	Ref	Expression
Hypotheses	sbceqbii.1	⊢ 𝐴 = 𝐵
	sbceqbii.2	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	sbceqbii	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbceqbii.1	⊢ 𝐴 = 𝐵
2		sbceqbii.2	⊢ ( 𝜑 ↔ 𝜓 )
3	2	abbii	⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 }
4	1 3	eleq12i	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐵 ∈ { 𝑥 ∣ 𝜓 } )
5		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
6		df-sbc	⊢ ( [ 𝐵 / 𝑥 ] 𝜓 ↔ 𝐵 ∈ { 𝑥 ∣ 𝜓 } )
7	4 5 6	3bitr4i	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜓 )