Metamath Proof Explorer


Theorem dfnul3OLD

Description: Obsolete version of dfnul4 as of 23-Sep-2024. (Contributed by NM, 25-Mar-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfnul3OLD
|- (/) = { x e. A | -. x e. A }

Proof

Step Hyp Ref Expression
1 pm3.24
 |-  -. ( x e. A /\ -. x e. A )
2 equid
 |-  x = x
3 1 2 2th
 |-  ( -. ( x e. A /\ -. x e. A ) <-> x = x )
4 3 con1bii
 |-  ( -. x = x <-> ( x e. A /\ -. x e. A ) )
5 4 abbii
 |-  { x | -. x = x } = { x | ( x e. A /\ -. x e. A ) }
6 dfnul2
 |-  (/) = { x | -. x = x }
7 df-rab
 |-  { x e. A | -. x e. A } = { x | ( x e. A /\ -. x e. A ) }
8 5 6 7 3eqtr4i
 |-  (/) = { x e. A | -. x e. A }