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 }