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	$⊢ Ⅎ y φ$
	Assertion	rmo6	$⊢ \exists^{*} x \in A φ \leftrightarrow (\exists z z \in A \to \exists y \in A \forall x \in A (φ \to x = y))$

Proof

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

Metamath Proof Explorer

Theorem rmo6

Proof