Theorem reu8nf

Description: Restricted uniqueness using implicit substitution. This version of reu8 uses a non-freeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022)

	Ref	Expression
Hypotheses	reu8nf.1	⊢ Ⅎ 𝑥 𝜓
	reu8nf.2	⊢ Ⅎ 𝑥 𝜒
	reu8nf.3	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
	reu8nf.4	⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
Assertion	reu8nf	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reu8nf.1	⊢ Ⅎ 𝑥 𝜓
2		reu8nf.2	⊢ Ⅎ 𝑥 𝜒
3		reu8nf.3	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
4		reu8nf.4	⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
5		nfv	⊢ Ⅎ 𝑤 𝜑
6	5 2 3	cbvreuw	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑤 ∈ 𝐴 𝜒 )
7	4	reu8	⊢ ( ∃! 𝑤 ∈ 𝐴 𝜒 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) )
8		nfcv	⊢ Ⅎ 𝑥 𝐴
9		nfv	⊢ Ⅎ 𝑥 𝑤 = 𝑦
10	1 9	nfim	⊢ Ⅎ 𝑥 ( 𝜓 → 𝑤 = 𝑦 )
11	8 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 )
12	2 11	nfan	⊢ Ⅎ 𝑥 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) )
13		nfv	⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) )
14	3	bicomd	⊢ ( 𝑥 = 𝑤 → ( 𝜒 ↔ 𝜑 ) )
15	14	equcoms	⊢ ( 𝑤 = 𝑥 → ( 𝜒 ↔ 𝜑 ) )
16		equequ1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦 ↔ 𝑥 = 𝑦 ) )
17	16	imbi2d	⊢ ( 𝑤 = 𝑥 → ( ( 𝜓 → 𝑤 = 𝑦 ) ↔ ( 𝜓 → 𝑥 = 𝑦 ) ) )
18	17	ralbidv	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
19	15 18	anbi12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) )
20	12 13 19	cbvrexw	⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )
21	6 7 20	3bitri	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) )