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	⊢ Ⅎ 𝑦 𝜑
Assertion	rmo6	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rmo6.1	⊢ Ⅎ 𝑦 𝜑
2		rmo5	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
3		nfcv	⊢ Ⅎ 𝑦 𝐴
4	3 1	nfrexw	⊢ Ⅎ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑
5	4	nfn	⊢ Ⅎ 𝑦 ¬ ∃ 𝑥 ∈ 𝐴 𝜑
6		idd	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
7		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
8	7	notbii	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
9		alnex	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
10	8 9	bitr4i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
11		pm2.21	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
12	11	expd	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
13	12	alimi	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
14	13	ralrid	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
15	10 14	sylbi	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
16	6 15	jctird	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ( 𝑦 ∈ 𝐴 → ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) ) )
17	5 16	eximd	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) ) )
18		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
19	17 18	imbitrrdi	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
20	1	reu6f	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
21		biimp	⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
22	21	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
23	22	reximi	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
24	20 23	sylbi	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
25	24	a1d	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
26	19 25	ja	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
27	2 26	sylbi	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
28		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
29	28	cbvexvw	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
30		exsimpl	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∃ 𝑥 𝑥 ∈ 𝐴 )
31	30	con3i	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝐴 → ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
32	29 31	sylnbir	⊢ ( ¬ ∃ 𝑦 𝑦 ∈ 𝐴 → ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
33	32 8	sylibr	⊢ ( ¬ ∃ 𝑦 𝑦 ∈ 𝐴 → ¬ ∃ 𝑥 ∈ 𝐴 𝜑 )
34		nrexrmo	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 )
35	33 34	syl	⊢ ( ¬ ∃ 𝑦 𝑦 ∈ 𝐴 → ∃* 𝑥 ∈ 𝐴 𝜑 )
36	1	rmo2i	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 ∈ 𝐴 𝜑 )
37	35 36	ja	⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) → ∃* 𝑥 ∈ 𝐴 𝜑 )
38	27 37	impbii	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
39		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
40	39	cbvexvw	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 ↔ ∃ 𝑤 𝑤 ∈ 𝐴 )
41		eleq1w	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
42	41	cbvexvw	⊢ ( ∃ 𝑤 𝑤 ∈ 𝐴 ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
43	40 42	bitri	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
44	43	imbi1i	⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) ↔ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )
45	38 44	bitri	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ) )