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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	wl-eujustlem1	⊢ ( ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-eujustlem1.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3	2	biimpcd	⊢ ( ¬ 𝜑 → ( 𝑥 = 𝑦 → ¬ 𝜓 ) )
4	3	aleximi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ¬ 𝜓 ) )
5		ax5e	⊢ ( ∃ 𝑥 ¬ 𝜓 → ¬ 𝜓 )
6	4 5	syl6	⊢ ( ∀ 𝑥 ¬ 𝜑 → ( ∃ 𝑥 𝑥 = 𝑦 → ¬ 𝜓 ) )
7	6	alimdv	⊢ ( ∀ 𝑥 ¬ 𝜑 → ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ 𝜓 ) )
8	7	com12	⊢ ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑦 ¬ 𝜓 ) )
9	2	biimprcd	⊢ ( ¬ 𝜓 → ( 𝑥 = 𝑦 → ¬ 𝜑 ) )
10	9	aleximi	⊢ ( ∀ 𝑦 ¬ 𝜓 → ( ∃ 𝑦 𝑥 = 𝑦 → ∃ 𝑦 ¬ 𝜑 ) )
11		ax5e	⊢ ( ∃ 𝑦 ¬ 𝜑 → ¬ 𝜑 )
12	10 11	syl6	⊢ ( ∀ 𝑦 ¬ 𝜓 → ( ∃ 𝑦 𝑥 = 𝑦 → ¬ 𝜑 ) )
13	12	alimdv	⊢ ( ∀ 𝑦 ¬ 𝜓 → ( ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 → ∀ 𝑥 ¬ 𝜑 ) )
14	13	com12	⊢ ( ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 → ( ∀ 𝑦 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) )
15	8 14	anbiim	⊢ ( ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 ) → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 ¬ 𝜓 ) )
16	15	notbid	⊢ ( ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 ) → ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜓 ) )
17		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
18		df-ex	⊢ ( ∃ 𝑦 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜓 )
19	16 17 18	3bitr4g	⊢ ( ( ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) )