Metamath Proof Explorer


Theorem excomimw

Description: Weak version of excomim . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025)

Ref Expression
Hypothesis excomimw.1 ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) )
Assertion excomimw ( ∃ 𝑥𝑦 𝜑 → ∃ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 excomimw.1 ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) )
2 1 notbid ( 𝑥 = 𝑧 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 2 alcomimw ( ∀ 𝑦𝑥 ¬ 𝜑 → ∀ 𝑥𝑦 ¬ 𝜑 )
4 3 con3i ( ¬ ∀ 𝑥𝑦 ¬ 𝜑 → ¬ ∀ 𝑦𝑥 ¬ 𝜑 )
5 2exnaln ( ∃ 𝑥𝑦 𝜑 ↔ ¬ ∀ 𝑥𝑦 ¬ 𝜑 )
6 2exnaln ( ∃ 𝑦𝑥 𝜑 ↔ ¬ ∀ 𝑦𝑥 ¬ 𝜑 )
7 4 5 6 3imtr4i ( ∃ 𝑥𝑦 𝜑 → ∃ 𝑦𝑥 𝜑 )