Theorem sbcbii

Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005)

	Ref	Expression
Hypothesis	sbcbii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbcbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2	1	a1i	⊢ ( ⊤ → ( 𝜑 ↔ 𝜓 ) )
3	2	sbcbidv	⊢ ( ⊤ → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )
4	3	mptru	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 )