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

Metamath Proof Explorer

Theorem rexreusng

Description: Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion rexreusng ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∃! 𝑥 ∈ { 𝐴 } 𝜑 ) )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 = 𝐴 )
2 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑
3 nfv ⊢ Ⅎ 𝑦 [ 𝐴 / 𝑥 ] 𝜑
4 2 3 nfan ⊢ Ⅎ 𝑦 ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 )
5 nfv ⊢ Ⅎ 𝑦 𝐴 = 𝐴
6 4 5 nfim ⊢ Ⅎ 𝑦 ( ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 = 𝐴 )
7 sbceq1a ⊢ ( 𝑦 = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
8 dfsbcq2 ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
9 7 8 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
10 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐴 ) )
11 9 10 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 = 𝐴 ) ) )
12 6 11 ralsngf ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝐴 } ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 = 𝐴 ) ) )
13 1 12 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑦 ∈ { 𝐴 } ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) )
14 nfcv ⊢ Ⅎ 𝑥 { 𝐴 }
15 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜑
16 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
17 15 16 nfan ⊢ Ⅎ 𝑥 ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 )
18 nfv ⊢ Ⅎ 𝑥 𝐴 = 𝑦
19 17 18 nfim ⊢ Ⅎ 𝑥 ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 )
20 14 19 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ { 𝐴 } ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 )
21 sbceq1a ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
22 21 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
23 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
24 22 23 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) ) )
25 24 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ { 𝐴 } ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐴 } ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) ) )
26 20 25 ralsngf ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐴 } ( ( [ 𝐴 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝐴 = 𝑦 ) ) )
27 13 26 mpbird ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
28 27 biantrud ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) ) )
29 reu2 ⊢ ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )
30 28 29 bitr4di ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∃! 𝑥 ∈ { 𝐴 } 𝜑 ) )