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

Metamath Proof Explorer

Theorem eusvnf

Description: Even if x is free in A , it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion eusvnf ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )

Proof

Step Hyp Ref Expression
1 euex ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ∃ 𝑦 ∀ 𝑥 𝑦 = 𝐴 )
2 nfcv ⊢ Ⅎ 𝑥 𝑧
3 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
4 3 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴
5 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
6 5 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝐴 ↔ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
7 2 4 6 spcgf ⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 𝑦 = 𝐴 → 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
8 7 elv ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
9 nfcv ⊢ Ⅎ 𝑥 𝑤
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐴
11 10 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴
12 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
13 12 eqeq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑦 = 𝐴 ↔ 𝑦 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
14 9 11 13 spcgf ⊢ ( 𝑤 ∈ V → ( ∀ 𝑥 𝑦 = 𝐴 → 𝑦 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) )
15 14 elv ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → 𝑦 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
16 8 15 eqtr3d ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
17 16 alrimivv ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → ∀ 𝑧 ∀ 𝑤 ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
18 sbnfc2 ⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
19 17 18 sylibr ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )
20 19 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )
21 1 20 syl ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )