Theorem compeq

Description: Equality between two ways of saying "the complement of A ". (Contributed by Andrew Salmon, 15-Jul-2011)

	Ref	Expression
Assertion	compeq	⊢ ( V ∖ 𝐴 ) = { 𝑥 ∣ ¬ 𝑥 ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		velcomp	⊢ ( 𝑥 ∈ ( V ∖ 𝐴 ) ↔ ¬ 𝑥 ∈ 𝐴 )
2	1	abbi2i	⊢ ( V ∖ 𝐴 ) = { 𝑥 ∣ ¬ 𝑥 ∈ 𝐴 }