This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 GG, 30-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 abf.1 
 |-  -. ph
2 1 bifal 
 |-  ( ph <-> F. )
3 2 abbii 
 |-  { x | ph } = { x | F. }
4 dfnul4 
 |-  (/) = { x | F. }
5 3 4 eqtr4i 
 |-  { x | ph } = (/)