Theorem sbcim1

Description: Distribution of class substitution over implication. One direction of sbcimg that holds for proper classes. (Contributed by NM, 17-Aug-2018) Avoid ax-10 , ax-12 . (Revised by SN, 26-Oct-2024)

	Ref	Expression
Assertion	sbcim1	|- ( [. A / x ]. ( ph -> ps ) -> ( [. A / x ]. ph -> [. A / x ]. ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / x ]. ( ph -> ps ) -> A e. _V )
2		dfsbcq2	|- ( y = A -> ( [ y / x ] ( ph -> ps ) <-> [. A / x ]. ( ph -> ps ) ) )
3		dfsbcq2	|- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
4		dfsbcq2	|- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
5	3 4	imbi12d	|- ( y = A -> ( ( [ y / x ] ph -> [ y / x ] ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
6	2 5	imbi12d	|- ( y = A -> ( ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) ) <-> ( [. A / x ]. ( ph -> ps ) -> ( [. A / x ]. ph -> [. A / x ]. ps ) ) ) )
7		sbi1	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
8	6 7	vtoclg	|- ( A e. _V -> ( [. A / x ]. ( ph -> ps ) -> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
9	1 8	mpcom	|- ( [. A / x ]. ( ph -> ps ) -> ( [. A / x ]. ph -> [. A / x ]. ps ) )