This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem excomw

Description: Weak version of excom and biconditional form of excomimw . Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026)

	Ref	Expression
Hypotheses	excomw.1	$⊢ x = w \to (φ \leftrightarrow ψ)$
	excomw.2	$⊢ y = z \to (φ \leftrightarrow χ)$
Assertion	excomw	$⊢ \exists x \exists y φ \leftrightarrow \exists y \exists x φ$

Step	Hyp	Ref	Expression
1		excomw.1	$⊢ x = w \to (φ \leftrightarrow ψ)$
2		excomw.2	$⊢ y = z \to (φ \leftrightarrow χ)$
3	1	excomimw	$⊢ \exists x \exists y φ \to \exists y \exists x φ$
4	2	excomimw	$⊢ \exists y \exists x φ \to \exists x \exists y φ$
5	3 4	impbii	$⊢ \exists x \exists y φ \leftrightarrow \exists y \exists x φ$