Theorem sbcbi2

Description: Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018) (Proof shortened by Wolf Lammen, 4-May-2023) Avoid ax-10 , ax-12 . (Revised by Steven Nguyen, 5-May-2024)

	Ref	Expression
Assertion	sbcbi2	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
2	1	eleq2d	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } ) )
3		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
4		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
5	2 3 4	3bitr4g	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )