Metamath Proof Explorer

Theorem dfnul4OLD

Description: Obsolete version of dfnul4 as of 23-Sep-2024. (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfnul4OLD 
|- (/) = { x | F. }

Proof

Step Hyp Ref Expression
1 dfnul2 
 |-  (/) = { x | -. x = x }
2 equid 
 |-  x = x
3 2 notnoti 
 |-  -. -. x = x
4 3 bifal 
 |-  ( -. x = x <-> F. )
5 4 abbii 
 |-  { x | -. x = x } = { x | F. }
6 1 5 eqtri 
 |-  (/) = { x | F. }