Metamath Proof Explorer


Theorem bj-spcimdvv

Description: Remove from spcimdv dependency on ax-7 , ax-8 , ax-10 , ax-11 , ax-12 ax-13 , ax-ext , df-cleq , df-clab (and df-nfc , df-v , df-or , df-tru , df-nf ) at the price of adding a disjoint variable condition on x , B (but in usages, x is typically a dummy, hence fresh, variable). For the version without this disjoint variable condition, see bj-spcimdv . (Contributed by BJ, 3-Nov-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-spcimdvv.1 ( 𝜑𝐴𝐵 )
bj-spcimdvv.2 ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
Assertion bj-spcimdvv ( 𝜑 → ( ∀ 𝑥 𝜓𝜒 ) )

Proof

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