Metamath Proof Explorer


Theorem bj-spcimdv

Description: Remove from spcimdv dependency on ax-9 , ax-10 , ax-11 , ax-13 , ax-ext , df-cleq (and df-nfc , df-v , df-or , df-tru , df-nf ). For an even more economical version, see bj-spcimdvv . (Contributed by BJ, 30-Nov-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-spcimdv.1
|- ( ph -> A e. B )
bj-spcimdv.2
|- ( ( ph /\ x = A ) -> ( ps -> ch ) )
Assertion bj-spcimdv
|- ( ph -> ( A. x ps -> ch ) )

Proof

Step Hyp Ref Expression
1 bj-spcimdv.1
 |-  ( ph -> A e. B )
2 bj-spcimdv.2
 |-  ( ( ph /\ x = A ) -> ( ps -> ch ) )
3 2 ex
 |-  ( ph -> ( x = A -> ( ps -> ch ) ) )
4 3 alrimiv
 |-  ( ph -> A. x ( x = A -> ( ps -> ch ) ) )
5 bj-elisset
 |-  ( A e. B -> E. x x = A )
6 exim
 |-  ( A. x ( x = A -> ( ps -> ch ) ) -> ( E. x x = A -> E. x ( ps -> ch ) ) )
7 5 6 syl5
 |-  ( A. x ( x = A -> ( ps -> ch ) ) -> ( A e. B -> E. x ( ps -> ch ) ) )
8 19.36v
 |-  ( E. x ( ps -> ch ) <-> ( A. x ps -> ch ) )
9 7 8 syl6ib
 |-  ( A. x ( x = A -> ( ps -> ch ) ) -> ( A e. B -> ( A. x ps -> ch ) ) )
10 4 1 9 sylc
 |-  ( ph -> ( A. x ps -> ch ) )