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 φ A B
bj-spcimdvv.2 φ x = A ψ χ
Assertion bj-spcimdvv φ x ψ χ

Proof

Step Hyp Ref Expression
1 bj-spcimdvv.1 φ A B
2 bj-spcimdvv.2 φ x = A ψ χ
3 2 ex φ x = A ψ χ
4 3 alrimiv φ x x = A ψ χ
5 elissetv A B x x = A
6 exim x x = A ψ χ x x = A x ψ χ
7 5 6 syl5 x x = A ψ χ A B x ψ χ
8 19.36v x ψ χ x ψ χ
9 7 8 syl6ib x x = A ψ χ A B x ψ χ
10 4 1 9 sylc φ x ψ χ