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