Metamath Proof Explorer


Theorem bj-ab0

Description: The class of sets verifying a falsity is the empty set (closed form of abf ). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ab0 x¬φx|φ=

Proof

Step Hyp Ref Expression
1 stdpc4 x¬φyx¬φ
2 sbn1 yx¬φ¬yxφ
3 1 2 syl x¬φ¬yxφ
4 df-clab yx|φyxφ
5 3 4 sylnibr x¬φ¬yx|φ
6 5 eq0rdv x¬φx|φ=