Description: A class abstraction of a collection of ordered pairs with a negated wff is the empty set. (Contributed by Peter Mazsa, 21-Oct-2019) (Proof shortened by Thierry Arnoux, 18-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | opabf.1 | |- -. ph |
|
| Assertion | opabf | |- { <. x , y >. | ph } = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opabf.1 | |- -. ph |
|
| 2 | 1 | gen2 | |- A. x A. y -. ph |
| 3 | opab0 | |- ( { <. x , y >. | ph } = (/) <-> A. x A. y -. ph ) |
|
| 4 | 2 3 | mpbir | |- { <. x , y >. | ph } = (/) |