Theorem sbcimdv

Description: Substitution analogue of Theorem 19.20 of Margaris p. 90 ( alim ). (Contributed by NM, 11-Nov-2005) (Revised by NM, 17-Aug-2018) (Proof shortened by JJ, 7-Jul-2021) Reduce axiom usage. (Revised by GG, 12-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sbcimdv.1	|- ( ph -> ( ps -> ch ) )
2		df-sbc	|- ( [. A / x ]. ps <-> A e. { x | ps } )
3		dfclel	|- ( A e. { x | ps } <-> E. y ( y = A /\ y e. { x | ps } ) )
4		df-clab	|- ( y e. { x | ps } <-> [ y / x ] ps )
5	4	anbi2i	|- ( ( y = A /\ y e. { x | ps } ) <-> ( y = A /\ [ y / x ] ps ) )
6	5	exbii	|- ( E. y ( y = A /\ y e. { x | ps } ) <-> E. y ( y = A /\ [ y / x ] ps ) )
7	2 3 6	3bitri	|- ( [. A / x ]. ps <-> E. y ( y = A /\ [ y / x ] ps ) )
8	7	biimpi	|- ( [. A / x ]. ps -> E. y ( y = A /\ [ y / x ] ps ) )
9	1	sbimdv	|- ( ph -> ( [ y / x ] ps -> [ y / x ] ch ) )
10	9	anim2d	|- ( ph -> ( ( y = A /\ [ y / x ] ps ) -> ( y = A /\ [ y / x ] ch ) ) )
11	10	eximdv	|- ( ph -> ( E. y ( y = A /\ [ y / x ] ps ) -> E. y ( y = A /\ [ y / x ] ch ) ) )
12		df-sbc	|- ( [. A / x ]. ch <-> A e. { x | ch } )
13		dfclel	|- ( A e. { x | ch } <-> E. y ( y = A /\ y e. { x | ch } ) )
14		df-clab	|- ( y e. { x | ch } <-> [ y / x ] ch )
15	14	anbi2i	|- ( ( y = A /\ y e. { x | ch } ) <-> ( y = A /\ [ y / x ] ch ) )
16	15	exbii	|- ( E. y ( y = A /\ y e. { x | ch } ) <-> E. y ( y = A /\ [ y / x ] ch ) )
17	12 13 16	3bitrri	|- ( E. y ( y = A /\ [ y / x ] ch ) <-> [. A / x ]. ch )
18	17	biimpi	|- ( E. y ( y = A /\ [ y / x ] ch ) -> [. A / x ]. ch )
19	8 11 18	syl56	|- ( ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) )