Description: Restricted existential quantification ( df-wl-rex ) allows a simplification, if we can assume all occurrences of x in A are bounded. (Contributed by Wolf Lammen, 25-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-dfrexf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-dfralf | ||
2 | 1 | notbid | |
3 | df-wl-rex | ||
4 | exnalimn | ||
5 | 2 3 4 | 3bitr4g |