reu6f

Description: Version of reu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BTernaryTau, 29-Sep-2026)

		Ref	Expression
	Hypothesis	reu6f.1	$⊢ Ⅎ y φ$
	Assertion	reu6f	$⊢ \exists! x \in A φ \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$

Proof

Step	Hyp	Ref	Expression
1		reu6f.1	$⊢ Ⅎ y φ$
2		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
3		19.28v	$⊢ \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \leftrightarrow (y \in A \land \forall x (x \in A \to (φ \leftrightarrow x = y)))$
4		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
5		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
6	4 5	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ))$
7		equequ1	$⊢ x = y \to (x = y \leftrightarrow y = y)$
8	6 7	bibi12d	$⊢ x = y \to (((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow ((y \in A \land [y/ x] φ) \leftrightarrow y = y))$
9		equid	$⊢ y = y$
10	9	tbt	$⊢ (y \in A \land [y/ x] φ) \leftrightarrow ((y \in A \land [y/ x] φ) \leftrightarrow y = y)$
11		simpl	$⊢ (y \in A \land [y/ x] φ) \to y \in A$
12	10 11	sylbir	$⊢ ((y \in A \land [y/ x] φ) \leftrightarrow y = y) \to y \in A$
13	8 12	biimtrdi	$⊢ x = y \to (((x \in A \land φ) \leftrightarrow x = y) \to y \in A)$
14	13	spimvw	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to y \in A$
15		ibar	$⊢ x \in A \to (φ \leftrightarrow (x \in A \land φ))$
16	15	bibi1d	$⊢ x \in A \to ((φ \leftrightarrow x = y) \leftrightarrow ((x \in A \land φ) \leftrightarrow x = y))$
17	16	biimprcd	$⊢ ((x \in A \land φ) \leftrightarrow x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
18	17	sps	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
19	14 18	jca	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
20	19	axc4i	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
21		biimp	$⊢ (φ \leftrightarrow x = y) \to (φ \to x = y)$
22	21	imim2i	$⊢ (x \in A \to (φ \leftrightarrow x = y)) \to (x \in A \to (φ \to x = y))$
23	22	impd	$⊢ (x \in A \to (φ \leftrightarrow x = y)) \to ((x \in A \land φ) \to x = y)$
24	23	adantl	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to ((x \in A \land φ) \to x = y)$
25	4	biimprcd	$⊢ y \in A \to (x = y \to x \in A)$
26	25	adantr	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to (x = y \to x \in A)$
27	26	imp	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to x \in A$
28		simplr	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
29		simpr	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to x = y$
30		biimpr	$⊢ (φ \leftrightarrow x = y) \to (x = y \to φ)$
31	28 29 30	syl6ci	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \to φ)$
32	27 31	jcai	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \land φ)$
33	32	ex	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to (x = y \to (x \in A \land φ))$
34	24 33	impbid	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to ((x \in A \land φ) \leftrightarrow x = y)$
35	34	alimi	$⊢ \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to \forall x ((x \in A \land φ) \leftrightarrow x = y)$
36	20 35	impbii	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
37		df-ral	$⊢ \forall x \in A (φ \leftrightarrow x = y) \leftrightarrow \forall x (x \in A \to (φ \leftrightarrow x = y))$
38	37	anbi2i	$⊢ (y \in A \land \forall x \in A (φ \leftrightarrow x = y)) \leftrightarrow (y \in A \land \forall x (x \in A \to (φ \leftrightarrow x = y)))$
39	3 36 38	3bitr4i	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
40	39	exbii	$⊢ \exists y \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow \exists y (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
41		nfv	$⊢ Ⅎ y x \in A$
42	41 1	nfan	$⊢ Ⅎ y (x \in A \land φ)$
43	42	euf	$⊢ \exists! x (x \in A \land φ) \leftrightarrow \exists y \forall x ((x \in A \land φ) \leftrightarrow x = y)$
44		df-rex	$⊢ \exists y \in A \forall x \in A (φ \leftrightarrow x = y) \leftrightarrow \exists y (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
45	40 43 44	3bitr4i	$⊢ \exists! x (x \in A \land φ) \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$
46	2 45	bitri	$⊢ \exists! x \in A φ \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$

Metamath Proof Explorer

Theorem reu6f

Proof