Theorem wl-eujustlem1

Description: Version of cbvexvw with references to ax-6 listed as antecedents. (Contributed by Wolf Lammen, 18-Feb-2026)

	Ref	Expression
Hypothesis	wl-eujustlem1.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	wl-eujustlem1	$$⊢\left(\forall y\exists xx=y\wedge \forall x\exists yx=y\right)\to \left(\exists x\phi \leftrightarrow \exists y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-eujustlem1.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2	1	notbid	$$⊢x=y\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	2	biimpcd	$$⊢\neg \phi \to \left(x=y\to \neg \psi \right)$$
4	3	aleximi	$$⊢\forall x\neg \phi \to \left(\exists xx=y\to \exists x\neg \psi \right)$$
5		ax5e	$$⊢\exists x\neg \psi \to \neg \psi$$
6	4 5	syl6	$$⊢\forall x\neg \phi \to \left(\exists xx=y\to \neg \psi \right)$$
7	6	alimdv	$$⊢\forall x\neg \phi \to \left(\forall y\exists xx=y\to \forall y\neg \psi \right)$$
8	7	com12	$$⊢\forall y\exists xx=y\to \left(\forall x\neg \phi \to \forall y\neg \psi \right)$$
9	2	biimprcd	$$⊢\neg \psi \to \left(x=y\to \neg \phi \right)$$
10	9	aleximi	$$⊢\forall y\neg \psi \to \left(\exists yx=y\to \exists y\neg \phi \right)$$
11		ax5e	$$⊢\exists y\neg \phi \to \neg \phi$$
12	10 11	syl6	$$⊢\forall y\neg \psi \to \left(\exists yx=y\to \neg \phi \right)$$
13	12	alimdv	$$⊢\forall y\neg \psi \to \left(\forall x\exists yx=y\to \forall x\neg \phi \right)$$
14	13	com12	$$⊢\forall x\exists yx=y\to \left(\forall y\neg \psi \to \forall x\neg \phi \right)$$
15	8 14	anbiim	$$⊢\left(\forall y\exists xx=y\wedge \forall x\exists yx=y\right)\to \left(\forall x\neg \phi \leftrightarrow \forall y\neg \psi \right)$$
16	15	notbid	$$⊢\left(\forall y\exists xx=y\wedge \forall x\exists yx=y\right)\to \left(\neg \forall x\neg \phi \leftrightarrow \neg \forall y\neg \psi \right)$$
17		df-ex	$$⊢\exists x\phi \leftrightarrow \neg \forall x\neg \phi$$
18		df-ex	$$⊢\exists y\psi \leftrightarrow \neg \forall y\neg \psi$$
19	16 17 18	3bitr4g	$$⊢\left(\forall y\exists xx=y\wedge \forall x\exists yx=y\right)\to \left(\exists x\phi \leftrightarrow \exists y\psi \right)$$