Metamath Proof Explorer


Theorem dvelimexcased

Description: Eliminate a disjoint variable condition from an existentially quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025)

Ref Expression
Hypotheses dvelimexcased.1 x φ
dvelimexcased.2 ¬ x x = y z φ
dvelimexcased.3 φ ¬ x x = y x ψ
dvelimexcased.4 φ ¬ x x = y z θ
dvelimexcased.5 φ ¬ x x = y z = x ψ θ
dvelimexcased.6 φ x x = y χ θ
dvelimexcased.7 φ z ψ
dvelimexcased.8 φ x χ
Assertion dvelimexcased φ x θ

Proof

Step Hyp Ref Expression
1 dvelimexcased.1 x φ
2 dvelimexcased.2 ¬ x x = y z φ
3 dvelimexcased.3 φ ¬ x x = y x ψ
4 dvelimexcased.4 φ ¬ x x = y z θ
5 dvelimexcased.5 φ ¬ x x = y z = x ψ θ
6 dvelimexcased.6 φ x x = y χ θ
7 dvelimexcased.7 φ z ψ
8 dvelimexcased.8 φ x χ
9 nfa1 x x x = y
10 1 9 nfan x φ x x = y
11 10 6 eximd φ x x = y x χ x θ
12 11 ex φ x x = y x χ x θ
13 8 12 mpid φ x x = y x θ
14 nfv z ¬ x x = y
15 14 2 nfan1c z φ ¬ x x = y
16 nfna1 x ¬ x x = y
17 1 16 nfan x φ ¬ x x = y
18 15 17 3 4 5 cbvex1v φ ¬ x x = y z ψ x θ
19 18 ex φ ¬ x x = y z ψ x θ
20 7 19 mpid φ ¬ x x = y x θ
21 13 20 pm2.61d φ x θ