Metamath Proof Explorer

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 ⊢∀xℲyφ→∃!xφ↔∃!yyxφ

Proof

Step Hyp Ref Expression
1 nfnf1 ⊢ℲyℲyφ
2 1 nfal ⊢Ⅎy∀xℲyφ
3 equsb3 ⊢vxx=u↔v=u
4 3 sblbis ⊢vxφ↔x=u↔vxφ↔v=u
5 nfa1 ⊢Ⅎx∀xℲyφ
6 sp ⊢∀xℲyφ→Ⅎyφ
7 5 6 nfsbd ⊢∀xℲyφ→Ⅎyvxφ
8 nfvd ⊢∀xℲyφ→Ⅎyv=u
9 7 8 nfbid ⊢∀xℲyφ→Ⅎyvxφ↔v=u
10 4 9 nfxfrd ⊢∀xℲyφ→Ⅎyvxφ↔x=u
11 sbequ ⊢v=y→vxφ↔x=u↔yxφ↔x=u
12 11 a1i ⊢∀xℲyφ→v=y→vxφ↔x=u↔yxφ↔x=u
13 2 10 12 cbvald ⊢∀xℲyφ→∀vvxφ↔x=u↔∀yyxφ↔x=u
14 nfv ⊢Ⅎvφ↔x=u
15 14 sb8 ⊢∀xφ↔x=u↔∀vvxφ↔x=u
16 15 bicomi ⊢∀vvxφ↔x=u↔∀xφ↔x=u
17 equsb3 ⊢yxx=u↔y=u
18 17 sblbis ⊢yxφ↔x=u↔yxφ↔y=u
19 18 albii ⊢∀yyxφ↔x=u↔∀yyxφ↔y=u
20 13 16 19 3bitr3g ⊢∀xℲyφ→∀xφ↔x=u↔∀yyxφ↔y=u
21 20 exbidv ⊢∀xℲyφ→∃u∀xφ↔x=u↔∃u∀yyxφ↔y=u
22 eu6 ⊢∃!xφ↔∃u∀xφ↔x=u
23 eu6 ⊢∃!yyxφ↔∃u∀yyxφ↔y=u
24 21 22 23 3bitr4g ⊢∀xℲyφ→∃!xφ↔∃!yyxφ