Description: Alternate definition of restricted universal quantification ( df-wl-rex ) when x and A are disjoint. (Contributed by Wolf Lammen, 25-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-dfrexv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-dfralv | ||
2 | 1 | notbii | |
3 | df-wl-rex | ||
4 | exnalimn | ||
5 | 2 3 4 | 3bitr4i |