Metamath Proof Explorer


Theorem opab0

Description: Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021)

Ref Expression
Assertion opab0
|- ( { <. x , y >. | ph } = (/) <-> A. x A. y -. ph )

Proof

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 )