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 ( 𝜑𝐴𝐵 )
bj-spcimdv.2 ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
Assertion bj-spcimdv ( 𝜑 → ( ∀ 𝑥 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 bj-spcimdv.1 ( 𝜑𝐴𝐵 )
2 bj-spcimdv.2 ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
3 2 ex ( 𝜑 → ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) )
4 3 alrimiv ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) )
5 bj-elisset ( 𝐴𝐵 → ∃ 𝑥 𝑥 = 𝐴 )
6 exim ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( 𝜓𝜒 ) ) )
7 5 6 syl5 ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) → ( 𝐴𝐵 → ∃ 𝑥 ( 𝜓𝜒 ) ) )
8 19.36v ( ∃ 𝑥 ( 𝜓𝜒 ) ↔ ( ∀ 𝑥 𝜓𝜒 ) )
9 7 8 syl6ib ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) → ( 𝐴𝐵 → ( ∀ 𝑥 𝜓𝜒 ) ) )
10 4 1 9 sylc ( 𝜑 → ( ∀ 𝑥 𝜓𝜒 ) )