Theorem sbcbii

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

	Ref	Expression
Hypothesis	sbcbii.1	|- ( ph <-> ps )
Assertion	sbcbii	|- ( [. A / x ]. ph <-> [. A / x ]. ps )

Proof

Step	Hyp	Ref	Expression
1		sbcbii.1	|- ( ph <-> ps )
2	1	a1i	|- ( T. -> ( ph <-> ps ) )
3	2	sbcbidv	|- ( T. -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )
4	3	mptru	|- ( [. A / x ]. ph <-> [. A / x ]. ps )