Description: Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | opab0 | |- ( { <. x , y >. | ph } = (/) <-> A. x A. y -. ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabn0 | |- ( { <. x , y >. | ph } =/= (/) <-> E. x E. y ph ) |
|
2 | df-ne | |- ( { <. x , y >. | ph } =/= (/) <-> -. { <. x , y >. | ph } = (/) ) |
|
3 | 2exnaln | |- ( E. x E. y ph <-> -. A. x A. y -. ph ) |
|
4 | 1 2 3 | 3bitr3i | |- ( -. { <. x , y >. | ph } = (/) <-> -. A. x A. y -. ph ) |
5 | 4 | con4bii | |- ( { <. x , y >. | ph } = (/) <-> A. x A. y -. ph ) |