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
|- ( x = z -> ( ph <-> ps ) )
Assertion excomimw
|- ( E. x E. y ph -> E. y E. x ph )

Proof

Step Hyp Ref Expression
1 excomimw.1
 |-  ( x = z -> ( ph <-> ps ) )
2 1 notbid
 |-  ( x = z -> ( -. ph <-> -. ps ) )
3 2 alcomimw
 |-  ( A. y A. x -. ph -> A. x A. y -. ph )
4 3 con3i
 |-  ( -. A. x A. y -. ph -> -. A. y A. x -. ph )
5 2exnaln
 |-  ( E. x E. y ph <-> -. A. x A. y -. ph )
6 2exnaln
 |-  ( E. y E. x ph <-> -. A. y A. x -. ph )
7 4 5 6 3imtr4i
 |-  ( E. x E. y ph -> E. y E. x ph )