Metamath Proof Explorer

Theorem abf

Description: A class abstraction determined by a false formula is empty. (Contributed by NM, 20-Jan-2012)

Ref Expression
Hypothesis abf.1 
|- -. ph
Assertion abf 
|- { x | ph } = (/)

Proof

Step Hyp Ref Expression
1 abf.1 
 |-  -. ph
2 ab0 
 |-  ( { x | ph } = (/) <-> A. x -. ph )
3 2 1 mpgbir 
 |-  { x | ph } = (/)