Metamath Proof Explorer


Theorem dvelimalcased

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

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

Proof

Step Hyp Ref Expression
1 dvelimalcased.1 x φ
2 dvelimalcased.2 ¬ x x = y z φ
3 dvelimalcased.3 φ ¬ x x = y x ψ
4 dvelimalcased.4 φ ¬ x x = y z θ
5 dvelimalcased.5 φ ¬ x x = y z = x ψ θ
6 dvelimalcased.6 φ x x = y χ θ
7 dvelimalcased.7 φ z ψ
8 dvelimalcased.8 φ x χ
9 nfa1 x x x = y
10 1 9 nfan x φ x x = y
11 10 6 alimd φ 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 cbv1v φ ¬ 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 θ