This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )