Metamath Proof Explorer


Theorem cbvreuw

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvreuw.1 yφ
cbvreuw.2 xψ
cbvreuw.3 x=yφψ
Assertion cbvreuw ∃!xAφ∃!yAψ

Proof

Step Hyp Ref Expression
1 cbvreuw.1 yφ
2 cbvreuw.2 xψ
3 cbvreuw.3 x=yφψ
4 nfv zxAφ
5 4 sb8euv ∃!xxAφ∃!zzxxAφ
6 sban zxxAφzxxAzxφ
7 6 eubii ∃!zzxxAφ∃!zzxxAzxφ
8 clelsb1 zxxAzA
9 8 anbi1i zxxAzxφzAzxφ
10 9 eubii ∃!zzxxAzxφ∃!zzAzxφ
11 nfv yzA
12 1 nfsbv yzxφ
13 11 12 nfan yzAzxφ
14 nfv zyAψ
15 eleq1w z=yzAyA
16 sbequ z=yzxφyxφ
17 2 3 sbiev yxφψ
18 16 17 bitrdi z=yzxφψ
19 15 18 anbi12d z=yzAzxφyAψ
20 13 14 19 cbveuw ∃!zzAzxφ∃!yyAψ
21 10 20 bitri ∃!zzxxAzxφ∃!yyAψ
22 5 7 21 3bitri ∃!xxAφ∃!yyAψ
23 df-reu ∃!xAφ∃!xxAφ
24 df-reu ∃!yAψ∃!yyAψ
25 22 23 24 3bitr4i ∃!xAφ∃!yAψ