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 -> ( ph <-> ps ) )
Assertion	wl-eujustlem1	|- ( ( A. y E. x x = y /\ A. x E. y x = y ) -> ( E. x ph <-> E. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		wl-eujustlem1.1	|- ( x = y -> ( ph <-> ps ) )
2	1	notbid	|- ( x = y -> ( -. ph <-> -. ps ) )
3	2	biimpcd	|- ( -. ph -> ( x = y -> -. ps ) )
4	3	aleximi	|- ( A. x -. ph -> ( E. x x = y -> E. x -. ps ) )
5		ax5e	|- ( E. x -. ps -> -. ps )
6	4 5	syl6	|- ( A. x -. ph -> ( E. x x = y -> -. ps ) )
7	6	alimdv	|- ( A. x -. ph -> ( A. y E. x x = y -> A. y -. ps ) )
8	7	com12	|- ( A. y E. x x = y -> ( A. x -. ph -> A. y -. ps ) )
9	2	biimprcd	|- ( -. ps -> ( x = y -> -. ph ) )
10	9	aleximi	|- ( A. y -. ps -> ( E. y x = y -> E. y -. ph ) )
11		ax5e	|- ( E. y -. ph -> -. ph )
12	10 11	syl6	|- ( A. y -. ps -> ( E. y x = y -> -. ph ) )
13	12	alimdv	|- ( A. y -. ps -> ( A. x E. y x = y -> A. x -. ph ) )
14	13	com12	|- ( A. x E. y x = y -> ( A. y -. ps -> A. x -. ph ) )
15	8 14	anbiim	|- ( ( A. y E. x x = y /\ A. x E. y x = y ) -> ( A. x -. ph <-> A. y -. ps ) )
16	15	notbid	|- ( ( A. y E. x x = y /\ A. x E. y x = y ) -> ( -. A. x -. ph <-> -. A. y -. ps ) )
17		df-ex	|- ( E. x ph <-> -. A. x -. ph )
18		df-ex	|- ( E. y ps <-> -. A. y -. ps )
19	16 17 18	3bitr4g	|- ( ( A. y E. x x = y /\ A. x E. y x = y ) -> ( E. x ph <-> E. y ps ) )