Theorem rmo6

Description: Alternate version of rmo2 where y has a restricted quantifier. The antecedent E. z z e. A on the right-hand side handles the case where A is empty. (Contributed by BTernaryTau, 29-Sep-2026)

	Ref	Expression
Hypothesis	rmo6.1	|- F/ y ph
Assertion	rmo6	|- ( E* x e. A ph <-> ( E. z z e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )

Proof

Step	Hyp	Ref	Expression
1		rmo6.1	|- F/ y ph
2		rmo5	|- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) )
3		nfcv	|- F/_ y A
4	3 1	nfrexw	|- F/ y E. x e. A ph
5	4	nfn	|- F/ y -. E. x e. A ph
6		idd	|- ( -. E. x e. A ph -> ( y e. A -> y e. A ) )
7		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
8	7	notbii	|- ( -. E. x e. A ph <-> -. E. x ( x e. A /\ ph ) )
9		alnex	|- ( A. x -. ( x e. A /\ ph ) <-> -. E. x ( x e. A /\ ph ) )
10	8 9	bitr4i	|- ( -. E. x e. A ph <-> A. x -. ( x e. A /\ ph ) )
11		pm2.21	|- ( -. ( x e. A /\ ph ) -> ( ( x e. A /\ ph ) -> x = y ) )
12	11	expd	|- ( -. ( x e. A /\ ph ) -> ( x e. A -> ( ph -> x = y ) ) )
13	12	alimi	|- ( A. x -. ( x e. A /\ ph ) -> A. x ( x e. A -> ( ph -> x = y ) ) )
14	13	ralrid	|- ( A. x -. ( x e. A /\ ph ) -> A. x e. A ( ph -> x = y ) )
15	10 14	sylbi	|- ( -. E. x e. A ph -> A. x e. A ( ph -> x = y ) )
16	6 15	jctird	|- ( -. E. x e. A ph -> ( y e. A -> ( y e. A /\ A. x e. A ( ph -> x = y ) ) ) )
17	5 16	eximd	|- ( -. E. x e. A ph -> ( E. y y e. A -> E. y ( y e. A /\ A. x e. A ( ph -> x = y ) ) ) )
18		df-rex	|- ( E. y e. A A. x e. A ( ph -> x = y ) <-> E. y ( y e. A /\ A. x e. A ( ph -> x = y ) ) )
19	17 18	imbitrrdi	|- ( -. E. x e. A ph -> ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
20	1	reu6f	|- ( E! x e. A ph <-> E. y e. A A. x e. A ( ph <-> x = y ) )
21		biimp	|- ( ( ph <-> x = y ) -> ( ph -> x = y ) )
22	21	ralimi	|- ( A. x e. A ( ph <-> x = y ) -> A. x e. A ( ph -> x = y ) )
23	22	reximi	|- ( E. y e. A A. x e. A ( ph <-> x = y ) -> E. y e. A A. x e. A ( ph -> x = y ) )
24	20 23	sylbi	|- ( E! x e. A ph -> E. y e. A A. x e. A ( ph -> x = y ) )
25	24	a1d	|- ( E! x e. A ph -> ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
26	19 25	ja	|- ( ( E. x e. A ph -> E! x e. A ph ) -> ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
27	2 26	sylbi	|- ( E* x e. A ph -> ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
28		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
29	28	cbvexvw	|- ( E. x x e. A <-> E. y y e. A )
30		exsimpl	|- ( E. x ( x e. A /\ ph ) -> E. x x e. A )
31	30	con3i	|- ( -. E. x x e. A -> -. E. x ( x e. A /\ ph ) )
32	29 31	sylnbir	|- ( -. E. y y e. A -> -. E. x ( x e. A /\ ph ) )
33	32 8	sylibr	|- ( -. E. y y e. A -> -. E. x e. A ph )
34		nrexrmo	|- ( -. E. x e. A ph -> E* x e. A ph )
35	33 34	syl	|- ( -. E. y y e. A -> E* x e. A ph )
36	1	rmo2i	|- ( E. y e. A A. x e. A ( ph -> x = y ) -> E* x e. A ph )
37	35 36	ja	|- ( ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) -> E* x e. A ph )
38	27 37	impbii	|- ( E* x e. A ph <-> ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
39		eleq1w	|- ( y = w -> ( y e. A <-> w e. A ) )
40	39	cbvexvw	|- ( E. y y e. A <-> E. w w e. A )
41		eleq1w	|- ( w = z -> ( w e. A <-> z e. A ) )
42	41	cbvexvw	|- ( E. w w e. A <-> E. z z e. A )
43	40 42	bitri	|- ( E. y y e. A <-> E. z z e. A )
44	43	imbi1i	|- ( ( E. y y e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) <-> ( E. z z e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )
45	38 44	bitri	|- ( E* x e. A ph <-> ( E. z z e. A -> E. y e. A A. x e. A ( ph -> x = y ) ) )