Metamath Proof Explorer


Theorem abf

Description: A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 abf.1 ¬ φ
2 ab0 x | φ = x ¬ φ
3 2 1 mpgbir x | φ =