Metamath Proof Explorer


Theorem dvelimalcasei

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

Ref Expression
Hypotheses dvelimalcasei.1 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
dvelimalcasei.2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜒 )
dvelimalcasei.3 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝜑𝜒 ) ) )
dvelimalcasei.4 ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓𝜒 ) )
dvelimalcasei.5 𝑧 𝜑
dvelimalcasei.6 𝑥 𝜓
Assertion dvelimalcasei 𝑥 𝜒

Proof

Step Hyp Ref Expression
1 dvelimalcasei.1 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
2 dvelimalcasei.2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜒 )
3 dvelimalcasei.3 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝜑𝜒 ) ) )
4 dvelimalcasei.4 ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓𝜒 ) )
5 dvelimalcasei.5 𝑧 𝜑
6 dvelimalcasei.6 𝑥 𝜓
7 nftru 𝑥
8 nfvd ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 ⊤ )
9 1 adantl ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜑 )
10 2 adantl ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜒 )
11 3 adantl ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜑𝜒 ) ) )
12 4 adantl ( ( ⊤ ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
13 5 a1i ( ⊤ → ∀ 𝑧 𝜑 )
14 6 a1i ( ⊤ → ∀ 𝑥 𝜓 )
15 7 8 9 10 11 12 13 14 dvelimalcased ( ⊤ → ∀ 𝑥 𝜒 )
16 15 mptru 𝑥 𝜒