Theorem reusngf

Description: Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023)

	Ref	Expression
Hypotheses	rexsngf.1	⊢ Ⅎ 𝑥 𝜓
	rexsngf.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	reusngf	⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rexsngf.1	⊢ Ⅎ 𝑥 𝜓
2		rexsngf.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑐 / 𝑥 ] 𝜑
4		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
5		sbceq1a	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
6		dfsbcq	⊢ ( 𝑤 = 𝑐 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑐 / 𝑥 ] 𝜑 ) )
7	3 4 5 6	reu8nf	⊢ ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∃ 𝑥 ∈ { 𝐴 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) )
8		nfcv	⊢ Ⅎ 𝑥 { 𝐴 }
9		nfv	⊢ Ⅎ 𝑥 𝐴 = 𝑐
10	3 9	nfim	⊢ Ⅎ 𝑥 ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 )
11	8 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 )
12	1 11	nfan	⊢ Ⅎ 𝑥 ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) )
13		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑐 ↔ 𝐴 = 𝑐 ) )
14	13	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) )
15	14	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ↔ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) )
16	2 15	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ) )
17	12 16	rexsngf	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ) )
18		nfv	⊢ Ⅎ 𝑐 ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 )
19		dfsbcq	⊢ ( 𝑐 = 𝐴 → ( [ 𝑐 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
20		eqeq2	⊢ ( 𝑐 = 𝐴 → ( 𝐴 = 𝑐 ↔ 𝐴 = 𝐴 ) )
21	19 20	imbi12d	⊢ ( 𝑐 = 𝐴 → ( ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ) )
22	18 21	ralsngf	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ) )
23	22	anbi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ↔ ( 𝜓 ∧ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ) ) )
24		eqidd	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 )
25	24	biantru	⊢ ( 𝜓 ↔ ( 𝜓 ∧ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 = 𝐴 ) ) )
26	23 25	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝜓 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝐴 = 𝑐 ) ) ↔ 𝜓 ) )
27	17 26	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } ( 𝜑 ∧ ∀ 𝑐 ∈ { 𝐴 } ( [ 𝑐 / 𝑥 ] 𝜑 → 𝑥 = 𝑐 ) ) ↔ 𝜓 ) )
28	7 27	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )