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 )