Theorem velcomp

Description: Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011)

	Ref	Expression
Assertion	velcomp	⊢ ( 𝑥 ∈ ( V ∖ 𝐴 ) ↔ ¬ 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		eldif	⊢ ( 𝑥 ∈ ( V ∖ 𝐴 ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴 ) )
3	1 2	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ 𝐴 ) ↔ ¬ 𝑥 ∈ 𝐴 )