Theorem sbceqbidf

Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018)

	Ref	Expression
Hypotheses	sbceqbidf.1	⊢ Ⅎ 𝑥 𝜑
	sbceqbidf.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	sbceqbidf.3	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	sbceqbidf	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ [ 𝐵 / 𝑥 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbceqbidf.1	⊢ Ⅎ 𝑥 𝜑
2		sbceqbidf.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		sbceqbidf.3	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
4	1 3	abbid	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } = { 𝑥 ∣ 𝜒 } )
5	2 4	eleq12d	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑥 ∣ 𝜒 } ) )
6		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
7		df-sbc	⊢ ( [ 𝐵 / 𝑥 ] 𝜒 ↔ 𝐵 ∈ { 𝑥 ∣ 𝜒 } )
8	5 6 7	3bitr4g	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ [ 𝐵 / 𝑥 ] 𝜒 ) )