This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )