Description: Restricted existential uniqueness ( df-wl-reu ) allows a simplification, if we can assume all occurrences of x in A are bounded. (Contributed by Wolf Lammen, 28-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-dfreuf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-dfrexf | ||
2 | wl-dfrmof | ||
3 | 1 2 | anbi12d | |
4 | df-wl-reu | ||
5 | df-eu | ||
6 | 3 4 5 | 3bitr4g |