Description: An alternate definition of restricted existential uniqueness ( df-wl-reu ) using substitution. (Contributed by Wolf Lammen, 28-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-dfreusb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-dfrexsb | ||
2 | wl-dfrmosb | ||
3 | 1 2 | anbi12i | |
4 | df-wl-reu | ||
5 | df-eu | ||
6 | 3 4 5 | 3bitr4i |