Metamath Proof Explorer


Theorem opab0

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

Ref Expression
Assertion opab0 xy|φ=xy¬φ

Proof

Step Hyp Ref Expression
1 opabn0 xy|φxyφ
2 df-ne xy|φ¬xy|φ=
3 2exnaln xyφ¬xy¬φ
4 1 2 3 3bitr3i ¬xy|φ=¬xy¬φ
5 4 con4bii xy|φ=xy¬φ