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	⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )