Metamath Proof Explorer


Theorem abf

Description: A class abstraction determined by a false formula is empty. (Contributed by NM, 20-Jan-2012) Avoid ax-8 , ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 30-Jun-2024)

Ref Expression
Hypothesis abf.1 ¬ φ
Assertion abf x | φ =

Proof

Step Hyp Ref Expression
1 abf.1 ¬ φ
2 1 bifal φ
3 2 abbii x | φ = x |
4 dfnul4 = x |
5 3 4 eqtr4i x | φ =