Theorem wl-sb8eut

Description: Substitution of variable in universal quantifier. Closed form of sb8eu . (Contributed by Wolf Lammen, 11-Aug-2019)

	Ref	Expression
Assertion	wl-sb8eut	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfnf1	⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝜑
2	1	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 Ⅎ 𝑦 𝜑
3		equsb3	⊢ ( [ 𝑣 / 𝑥 ] 𝑥 = 𝑢 ↔ 𝑣 = 𝑢 )
4	3	sblbis	⊢ ( [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ( [ 𝑣 / 𝑥 ] 𝜑 ↔ 𝑣 = 𝑢 ) )
5		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 Ⅎ 𝑦 𝜑
6		sp	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝜑 )
7	5 6	nfsbd	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 [ 𝑣 / 𝑥 ] 𝜑 )
8		nfvd	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝑣 = 𝑢 )
9	7 8	nfbid	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ( [ 𝑣 / 𝑥 ] 𝜑 ↔ 𝑣 = 𝑢 ) )
10	4 9	nfxfrd	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) )
11		sbequ	⊢ ( 𝑣 = 𝑦 → ( [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ) )
12	11	a1i	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( 𝑣 = 𝑦 → ( [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ) ) )
13	2 10 12	cbvald	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑣 [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ) )
14		nfv	⊢ Ⅎ 𝑣 ( 𝜑 ↔ 𝑥 = 𝑢 )
15	14	sb8	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∀ 𝑣 [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) )
16	15	bicomi	⊢ ( ∀ 𝑣 [ 𝑣 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑢 ) )
17		equsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑢 ↔ 𝑦 = 𝑢 )
18	17	sblbis	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑢 ) )
19	18	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑢 ) )
20	13 16 19	3bitr3g	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑢 ) ) )
21	20	exbidv	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑢 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑢 ) ↔ ∃ 𝑢 ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑢 ) ) )
22		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑢 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑢 ) )
23		eu6	⊢ ( ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑢 ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑢 ) )
24	21 22 23	3bitr4g	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )