Definition df-compl 3213

Description: Define the complement of a class. Compare nic-dfneg 1435. (Contributed by SF, 10-Jan-2015.)

Assertion

Ref	Expression
df-compl	⊢ ∼ A = (A ⩃ A)

Detailed syntax breakdown of Definition df-compl

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	ccompl 3206	. 2 class ∼ A
3	1, 1	cnin 3205	. 2 class (A ⩃ A)
4	2, 3	wceq 1642	1 wff ∼ A = (A ⩃ A)

This definition is referenced by:  elcomplg  3219  nfcompl  3230  compleq  3244  complexg  4100