Theorem sbcbidv

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014) Drop ax-12 . (Revised by Gino Giotto, 1-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		sbcbidv.1	|- ( ph -> ( ps <-> ch ) )
2		eqidd	|- ( ph -> A = A )
3	2 1	sbceqbid	|- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )